nLab cohesive homotopy type theory

under construction

Idea

By cohesive homotopy type theory one will mean a modal homotopy type theory implementing cohesive homotopy theory via an adjoint triple of modal operators (shape modality $\dashv$ flat modality $\dashv$ sharp modality), hence with categorical semantics in cohesive $\infty$-toposes.

A first formulation of cohesive homotopy type theory [Schreiber & Shulman (2012)] added the required adjoint triple of modal operators as axioms to plain homotopy type theory.

Another approach [Shulman (2015)] is to change the underlying rules of dependent type theory itself by adjoining syntax for flat-modal contexts (“crisp contexts”).

This second approach, via a modified type theory with crisp contexts (which has meanwhile be implemented in actual proof assistants such as Agda-flat), better lends itself to producing proofs internal to the theory and is what most authors now mean by (real-)cohesive homotopy type theory, see e.g. developments in: Myers (2019), Myers (2021), Myers & Riley (2023).

In any case, Cohesive homotopy type theory is an axiomatic theory of the higher geometry of cohesive homotopy theory, i.e. of the homotopy theory of differential topology:

In its categorical semantics, the types in cohesive HoTT are interpreted as cohesive homotopy types, hence as cohesive ∞-groupoids, such as for instance smooth ∞-groupoids. See also at motivation for cohesive toposes for a non-technical discussion.

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$$

called

• shape modality$\dashv$ flat modality $\dashv$ sharp modality,

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

$$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

$$\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 \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]$ 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]$ as equipped even with its canonical structure of a smooth manifold (with boundary).

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

As such, the canonical map $\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]$ exists as a type that behaves as the interval in differential geometry, and where $\mathbf{\Pi}(I)$ is equivalent to the unit type.

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

In particular, the smooth circle $S^1$ in this model is a 0-type such that $\mathbf{\Pi}(S^1)$ is the 1-type $\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 $\mathbb{Z} \hookrightarrow \mathbb{A}^1$ such that $\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.

Cohomology

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

Flat cohomology and local systems

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

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

(…)

de Rham cohomology

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

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

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

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

Coq-code:

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.

(…)

Related concepts

• real-cohesive homotopy type theory

• A1-cohesive homotopy type theory

• geometric homotopy type theory

• modal homotopy type theory

• stable homotopy type

• differential homotopy type theory

References

First discussion of a (homotopy) type theoretic formulation of the modal cohesive homotopy theory (adopting terminology from Lawvere 2007 ) considered in

• Urs Schreiber, differential cohomology in a cohesive topos (arXiv:1310.7930)

was given in

• Urs Schreiber, Mike Shulman, Quantum gauge field theory in Cohesive homotopy type theory, EPTCS 158 (2014) 109-126 [arXiv:1408.0054, doi:10.4204/EPTCS.158.8]

following

• Mike Shulman, Internalizing the external, or The Joys of Codiscreteness (blog post)

by adding axioms for the adjoint triple of modal operators to plain homotopy type theory.

See also broader discussion in:

• Urs Schreiber, Modern Physics formalized in Modal Homotopy Type Theory (2016)

• David Corfield, Chap. 5 of Modal Homotopy Type Theory, Oxford University Press (2020) [ISBN:9780198853404]

Another type-theoretic formulation of cohesive homotopy theory, now obtained by changing the rewrite rules of type theory itself – adding a syntactic notion of flat-modal (“crisp”) contexts:

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science 28 6 (2018) 856-941 lbrack;arXiv:1509.07584, doi:10.1017/S0960129517000147]

following a general pattern for modal type theory laid out in

• Dan Licata, Mike Shulman, Adjoint logic with a 2-category of modes, in Logical Foundations of Computer Science 2016, Lecture Notes in Computer Science 9537 (2016) [doi:10.1007/978-3-319-27683-0_16, pdf, slides]

with exposition in:

• Mike Shulman, Comonadic modalities and cohesion, talk at Geometry in Modal Homotopy Type Theory, 2019 (pdf slides, talk recording)

This approach (also “real cohesive type theory”) is now what most people refer to when speaking of cohesive homotopy type theory.

Notice that at this point there is no proof assistant that actually implements the shape modality this way, only the system consisting of flat modality $\dashv$ sharp modality (spatial type theory) runs on computers: eg. via Agda-flat.

Discussion of a fragment of differential cohesive homotopy type theory with Agda-flat:

• Felix Wellen, Cartan Geometry in Modal Homotopy Type Theory (arXiv:1806.05966, thesis pdf)

Further development of (real-)cohesive homotopy type theory:

• David Jaz Myers, Good Fibrations through the Modal Prism, Higher Structures 6 1 (2022) 212–255 [arXiv:1908.08034v2, higher-structures:Vol6Iss1/Myers]

Formalization of the shape/flat-fracture square (differential cohomology hexagon):

• David Jaz Myers, Modal Fracture of Higher Groups [arXiv:2106.15390]

  also: talk at CMU-HoTT Seminar, 2021 (pdf, pdf)

Discussion of pairs of commuting cohesive structures (such as the combination of real cohesion and equivariant relevant for differential orbifold cohomology:

• David Jaz Myers, Mitchell Riley, Commuting Cohesions [arXiv:2301.13780]

Exposition in:

• David Jaz Myers, Simplicial, Differential, and Equivariant Homotopy Type Theory, talk at CQTS (Jan 2023) [video: rec]