This post is to alert the members of the HoTT community to some exciting recent developments over at the n-Category Cafe.
First, some background. Some of us (perhaps many) believe that HoTT should eventually be able to function as the internal language of an 
-topos, in the same way that extensional type theory provides an internal language for ordinary topos theory. The basic structure is already there: any -topos can be presented by a model category, whose (acyclic cofibration, fibration) factorization system should model identity types. Peter Lumsdaine and I are working on modeling higher inductive types in such a model category; univalence is a thorny problem.
However, we don’t have to wait for the details of this interpretation to be nailed down to start using it. We can start using HoTT “internally” to a class of -toposes by adding axioms that represent properties or structure possessed by such toposes, akin to how we can do synthetic differential geometry or synthetic domain theory “synthetically” without having a particular topos in mind as a model.
I have thought for a while that Urs Schrieber’s notion of cohesive -topos would be a good candidate for such development. The notion of cohesive 1-topos (or, more generally, cohesive category over a base) is due to Lawvere: it is a connected, locally connected, local topos E satisfying some additional axioms. This essentially means that in its global-sections geometric morphism to Set, the inverse image functor (called Disc) admits a further left adjoint (called 
), and the direct image functor (called 
) a further right adjoint (called Codisc), and moreover Disc and (equivalently) Codisc are fully faithful.
The intuition is that the objects of E are “spaces” — sets equipped with some “cohesion”, such as a topology, a smooth structure, etc. The functor gives the underlying set of points of a space; Disc equips a set with “discrete cohesion”; Codisc equips it with “codiscrete cohesion”; and computes the set of connected components of a space.
A cohesive -topos is similar, but in the world of -categories: it is an -topos whose global-sections geometric morphism to 
–Gpd (the -topos corresponding to Set) is part of a 4-term adjoint string, where the inverse image functor Disc is fully faithful (as is the other functor in the same direction, Codisc). Now the leftmost adjoint is 
(or just 
), the fundamental -groupoid of a “space”.
Now, while all of this structure as stated talks about the relationship of one -topos to another, a useful fragment of it can be phrased purely insude the -topos E, and thereby also inside homotopy type theory (regarded as the internal language of such an E). The fully faithful functors Disc and Codisc can be regarded as equipping E with full subcategories of objects called “discrete” and “codiscrete”, respectively, and the existence of the various adjoints means that the discrete objects are both reflective and coreflective, while the codiscrete objects are reflective. There is a further compatibility condition which ensures that the category of discrete objects is canonically equivalent to the category of codiscrete ones, and that the two “global sections” functors agree modulo this equivalence.
Note that nothing in these axioms, phrased elementarily in terms of E, asserts that the category of discrete objects “is” –Gpd. Of course, that fact is not visible to the internal logic of E. Similar sorts of “internalization of the base topos” has also been used in ordinary topos theory, for instance in Awodey and Kishida’s interpretation of first-order modal logic in a topos of sheaves. (This suggests that perhaps “cohesion” can be regarded as a sort of “modality”.)
Anyway, the point is: a recent discussion at the n-Cafe, leading up to the formulation of these axioms in HoTT, can be found in the comments to this post. Since Urs has found that a good deal of formal differential geometry can be developed inside a cohesive -topos (perhaps augmented with some additional axioms, akin to SDG), this raises the possibility of formalizing all of that inside HoTT and Coq/Agda. I believe Urs is now pushing ahead with such a project.
