|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
Cohesive homotopy type theory is an axiomatic theory of higher geometry, the pairing of geometry in general and of differential geometry in particular with homotopy theory. The objects or types that it describes are cohesive homotopy types, hence cohesive ∞-groupoids, such as for instance smooth ∞-groupoids. See also at motivation for cohesive toposes for a non-technical discussion.
To the extent that plain homotopy type theory is a formalization of homotopy theory in that it is the internal language of an (∞,1)-topos, cohesive homotopy type theory is the internal language of a cohesive (∞,1)-topos.
One way to arrive at cohesive homotopy type theory is to start with the external axioms for cohesion on a given topos in terms of an adjoint quadruple of functors on the given topos and attempt to formulate them instead in the internal Mitchell-Bénabou type theory language of the topos. This fails, since for formulating the reflective subcategories of discrete objects and codiscrete objects internally one needs instead of the type of propositions a full type of types, as exists only in homotopy type theory. Passing to this, the axioms for cohesion can be formulated (Shulman) and are automatically that of homotopy cohesion.
Coq code at Codiscrete.v
for the reflector into codiscrete objects.
The homotopy type theory of the codiscrete objects we call the external theory.
The coreflector from discrete objects we write
for the reflector into discrete objects.
Before looking at the consequences of the axioms formally, we mention some example phenomena to illustrate the meaning of the axioms.
We indicate one central aspect of geometric homotopy theory that is not visible in plain homotopy type theory, but is captured by its cohesive refinement.
The standard interval in topological spaces plays two rather different roles, depending on what kind of equivalence between spaces is considered. To make this more vivid, it serves to think of as equipped even with its canonical structure of a smooth manifold (with boundary).
The canonical map to the point is certainly not a diffeomorphism, and from the point of view of differential geometry the interval carries non-trivial structure. Notably its endpoints are not equivalent points (terms) in differential geometry, but are distinct. From the point of view of differential geometry the interval is a homotopy 0-type (has h-level 2) – but one that is in some way equipped with geometric structure.
This geometric structure, however, induces also a notion of geometric paths in the interval, such that any two of its points are connected by such a path, after all. In other words, one can form the smooth fundamental ∞-groupoid of the interval and regard that as a homotopy type without further geometric structure (a discrete ∞-groupoid). This is an interval type, while itself is not.
As such, the canonical map is an equivalence after all, namely a weak homotopy equivalence. Therefore, after application of , what used to be a geometric 0-type becomes a (-1)-type and actually a (-2)-type (h-level 0) – up to equivalence the interval type, but without any geometry.
This latter property is what makes the interval important in bare homotopy theory, where it serves to model notions such as cylinder objects, left homotopies, etc. The former property, however, is what makes the interval important in geometry, where it serves to model Cartesian spaces, manifolds, etc.
In cohesive homotopy type theory these two roles of the interval can both be seen, via the reflective embedding of discrete objects, and the transition between them is present, via the fundamental ∞-groupoid reflector .
Specifically, there is a model for homotopy cohesion, called Smooth∞Grpd, in which smooth manifolds (with boundary) are fully faithfully embedded, where hence exists as a type that behaves as the interval in differential geometry, and where is equivalent to the unit type.
More generally, in this model every smooth manifold is a homotopy 0-type/0-truncated object, but the type is a discrete ∞-groupoid whose homotopy type is that of the topological space underlying , as regarded in the standard homotopy category of topological spaces.
We discuss implications of the axioms of cohesive homotopy type theory and go through the discussion of the various structures in a cohesive (∞,1)-topos.
Require Import Homotopy Subtopos Codiscrete LocalTopos CohesiveTopos. Hypothesis BG : Type. Hypothesis BG_is_0connected : is_contr (pi0 BG). Hypothesis pt : BG. Definition flat_dR : #Type := ipullback ([[fun _:unit => pt]]) (from_flat ([BG])).
A formalization in homotopy type theory with adjoint logic added is in
In the pseudocode formerly known as traditional mathematics, homotopy cohesion is discussed in