cohesive homotopy type theory

under construction


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Cohesive \infty-Toposes

cohesive topos

cohesive (∞,1)-topos

cohesive homotopy type theory



Presentation over a site

Structures in a cohesive (,1)(\infty,1)-topos

structures in a cohesive (∞,1)-topos

Structures with infinitesimal cohesion

infinitesimal cohesion?




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.

The Axioms

We discuss the formulation in homotopy type theory of the internal axioms on a cohesive (∞,1)-topos.

Cohesive homotopy type theory is a modal type theory which adds to homotopy type theory an adjoint triple of modalities

ʃ ʃ \dashv \flat \dashv \sharp


where ʃʃ and \sharp are idempotent monads and where \flat is an idempotent comonad, subject to some compatibility condition.

A) Codiscrete objects

Axiom A. The ambient homotopy type theory has a left-exact reflective sub-(∞,1)-category, to be called the base (∞,1)-topos “of codiscrete objects”.

Coq code at Codiscrete.v

We write

XX X \to \sharp X

for the reflector into codiscrete objects.

The homotopy type theory of the codiscrete objects we call the external theory.

B) Discrete objects

Axiom B. There is also a coreflective sub-(∞,1)-category of discrete objects such that with the codiscrete reflection it makes the ambient theory that of a local (∞,1)-topos.

Coq code at LocalTopos.v.

The coreflector from discrete objects we write

AA. \flat A \to A \,.

C) Cohesion

Axiom C The discrete objects are also reflective, the reflector is left adjoint to the coreflector and preserves product types.

Coq code at CohesiveTopos.v.

We write

XΠX X \to \Pi X

for the reflector into discrete objects.

Example phenomena

Before looking at the consequences of the axioms formally, we mention some example phenomena to illustrate the meaning of the axioms.

Geometric spaces and their cohesive homotopy types

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 I=[0,1]I = [0,1] 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 [0,1][0,1] as equipped even with its canonical structure of a smooth manifold (with boundary).

The canonical map I*I \to * 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 0,1:I0,1 : I 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 Π(I)\Pi(I) of the interval and regard that as a homotopy type without further geometric structure (a discrete ∞-groupoid). This Π(I)\Pi(I) is an interval type, while II itself is not.

As such, the canonical map Π(I)*\Pi(I) \to * is an equivalence after all, namely a weak homotopy equivalence. Therefore, after application of Π\Pi, 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 Π\mathbf{\Pi}.

Specifically, there is a model for homotopy cohesion, called Smooth∞Grpd, in which smooth manifolds (with boundary) are fully faithfully embedded, where hence I=[0,1]I = [0,1] exists as a type that behaves as the interval in differential geometry, and where Π(I)\mathbf{\Pi}(I) is equivalent to the unit type.

More generally, in this model every smooth manifold XX is a homotopy 0-type/0-truncated object, but the type Π(X)\mathbf{\Pi}(X) is a discrete ∞-groupoid whose homotopy type is that of the topological space underlying XX, as regarded in the standard homotopy category of topological spaces.

In particular, the smooth circle S 1S^1 in this model is a 0-type such that Π(S 1)\mathbf{\Pi}(S^1) is the 1-type B\mathbf{B}\mathbb{Z} (the delooping groupoid of the integers).

One can turn this around and axiomatize a continuum line object in cohesive homotopy type theory as a ring object 𝔸 1\mathbb{Z} \hookrightarrow \mathbb{A}^1 such that Π(𝔸 1)*\mathbf{\Pi}(\mathbb{A}^1) \simeq *.

Structures in cohesive homotopy type theory

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.


For XX and AA two types, the externalization (XA)\sharp(X \to A) of the function type XAX \to A is the type of cocycles on XX with coefficients in AA. Its h-level 2 truncation τ 0(XY)\tau_0 \sharp(X \to Y) is the cohomology of XX with coefficients in AA.

Flat cohomology and local systems

We give the Coq-formalization of Flat cohomology and local systems.

For AA a type, we say that cohomology with coefficients in A\flat A is flat cohomology. A cocycle term c:(XA)c : \sharp(X \to \flat A) is called a local system of coefficients AA on XX.


de Rham cohomology

We give the Coq-formalization of intrinsic de Rham cohomology.

Let A=BGA = \mathbf{B}G be a connected type.

The homotopy fiber type of the coreflection BGBG\flat \mathbf{B}G \to \mathbf{B}G we call the de Rham coefficient type of GG, denoted dRBG\flat_{dR} \mathbf{B}G. So there is a fiber sequence

dRBGBGBG. \flat_{dR} \mathbf{B}G \to \flat \mathbf{B}G \to \mathbf{B}G \,.


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])).

Differential cohomology

We give the Coq-formalization of Differential cohomology.



A survey with discussion of applications to gauge theory and quantum field theory is at

The formulation of axiomatic cohesion on 1-categories is due to Bill Lawvere, see there for a detailed bibliography.

The Coq formalization of axiomatic homotopy cohesion is discussed in

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

See also

Revised on March 21, 2016 04:55:31 by Ingo Blechschmidt (