nLab cohesive homotopy type theory

Contents

under construction

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

semantics

Cohesive \infty-Toposes

Contents

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

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.

As a multimodal type theory

There is another way to define cohesive homotopy type theory, as a multimodal type theory. Multimodal type theories were first introduced in Gratzer, Kavvos, Nuyts, & Birkedal 2021 and consists of a strict 2-category \mathcal{M} called the mode theory, whose objects are called modes and whose 1-cells are called modalities. For each mode mm \in \mathcal{M}, there is a type theory at mode mm, and for each 1-cell between objects there is a type theoretic modality in the type theory, which comes with its associated context lock.

The mode theory of cohesion

The mode theory \mathcal{M} of cohesive homotopy type theory consists of

  • two modes, the crisp or discrete mode 𝒹\mathcal{d} \in \mathcal{M} and the cohesive mode 𝒸\mathcal{c} \in \mathcal{M},

  • 1-cells p !,p *:𝒸𝒹p_!, p_*:\mathcal{c} \to \mathcal{d} and p *,p !:𝒹𝒸p^*, p^!:\mathcal{d} \to \mathcal{c},

  • 2-cells

    • η p !p *:id 𝒸p *p !\eta_{p_! \dashv p^*}: \mathrm{id}_\mathcal{c} \Rightarrow p^* \circ p_!

    • ϵ p !p *:p !p *id 𝒹\epsilon_{p_! \dashv p^*}: p_! \circ p^* \Rightarrow \mathrm{id}_\mathcal{d}

    • η p *p *:id 𝒹p *p *\eta_{p^* \dashv p_*}: \mathrm{id}_\mathcal{d} \Rightarrow p_* \circ p^*

    • ϵ p *p *:p *p *id 𝒸\epsilon_{p^* \dashv p_*}: p^* \circ p_* \Rightarrow \mathrm{id}_\mathcal{c}

    • η p *p !:id 𝒸p !p *\eta_{p_* \dashv p^!}: \mathrm{id}_\mathcal{c} \Rightarrow p^! \circ p_*

    • ϵ p *p !:p *p !id 𝒹\epsilon_{p_* \dashv p^!}: p_* \circ p^! \Rightarrow \mathrm{id}_\mathcal{d}

  • which satisfy the following triangle identities:

    • p *ϵ p !p *η p !p *p *=id p *p^* \epsilon_{p_! \dashv p^*} \cdot \eta_{p_! \dashv p^*} p^* = \mathrm{id}_{p^*}

    • ϵ p !p *p !p !η p !p *=id p !\epsilon_{p_! \dashv p^*} p_! \cdot p_! \eta_{p_! \dashv p^*} = \mathrm{id}_{p_!}

    • p *ϵ p *p *η p *p *p *=id p *p_* \epsilon_{p^* \dashv p_*} \cdot \eta_{p^* \dashv p_*} p_* = \mathrm{id}_{p_*}

    • ϵ p *p *p *p *η p *p *=id p *\epsilon_{p^* \dashv p_*} p^* \cdot p^* \eta_{p^* \dashv p_*} = \mathrm{id}_{p^*}

    • p !ϵ p *p !η p *p !p !=id p !p^! \epsilon_{p_* \dashv p^!} \cdot \eta_{p_* \dashv p^!} p^! = \mathrm{id}_{p^!}

    • ϵ p *p !p *p *η p *p !=id p *\epsilon_{p_* \dashv p^!} p_* \cdot p_* \eta_{p_* \dashv p^!} = \mathrm{id}_{p_*}

which makes the 1-cells into an adjoint quadruple

p !p *p *p !p_! \dashv p^* \dashv p_* \dashv p^!

The notations for the adjoint quadruple are derived from the introduction of Shulman 2015, but are traditionally expressed as

ΠDiscΓCodisc\Pi \dashv \mathrm{Disc} \dashv \Gamma \dashv \mathrm{Codisc}

(i.e. see cohesive infinity-topos). However, we do not use the above notations because Π\Pi conflicts with the use of Π\Pi for the dependent product type (i.e. Πx:A.B(x)\Pi x:A.B(x)) and Γ\Gamma conflicts with the use of Γ\Gamma to express arbitrary contexts in inference rules in dependent type theory.

The sharp, flat, and shape endo-modalities on the cohesive mode can be defined as composites of the modalities above:

p *p !:𝒸𝒸p *p *:𝒸𝒸ʃp !p *:𝒸𝒸\sharp \coloneqq p_* \circ p^!:\mathcal{c} \to \mathcal{c} \qquad \flat \coloneqq p_* \circ p^*:\mathcal{c} \to \mathcal{c} \qquad \esh \coloneqq p_! \circ p^*:\mathcal{c} \to \mathcal{c}

yielding the adjoint triple

ʃ\esh \dashv \flat \dashv \sharp

The modal type theory

In the multimodal type theory associated with cohesive homotopy type theory, there are two type judgments:

  • Atypeat𝒹A \; \mathrm{type} \; \mathrm{at} \; \mathcal{d} which says that AA is a type in the crisp mode;

  • Atypeat𝒸A \; \mathrm{type} \; \mathrm{at} \; \mathcal{c} which says that AA is a type in the cohesive mode.

Similarly, there are two term judgments:

  • a:Aat𝒹a:A \; \mathrm{at} \; \mathcal{d} which says that aa is a term of type AA in the crisp mode;

  • a:Aat𝒸a:A \; \mathrm{at} \; \mathcal{c} which says that aa is a term of type AA in the cohesive mode.

and two context judgments:

  • Γctxat𝒹\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d} which says that Γ\Gamma is a context in the crisp mode;

  • Γctxat𝒸\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c} which says that Γ\Gamma is a context in the cohesive mode.

as well as two separate judgments each for judgmental equality of types and terms:

  • ABtypeat𝒹A \equiv B \; \mathrm{type} \; \mathrm{at} \; \mathcal{d} which says that AA and BB are judgmentally equal types in the crisp mode;

  • ABtypeat𝒸A \equiv B \; \mathrm{type} \; \mathrm{at} \; \mathcal{c} which says that AA and BB are judgmentally equal types in the cohesive mode;

  • ab:Aat𝒹a \equiv b:A \; \mathrm{at} \; \mathcal{d} which says that aa and bb are judgmentally equal terms of type AA in the crisp mode;

  • ab:Aat𝒸a \equiv b:A \; \mathrm{at} \; \mathcal{c} which says that aa and bb are judgmentally equal terms of type AA in the cohesive mode.

  • ΓΔctxat𝒹\Gamma \equiv \Delta \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d} which says that Γ\Gamma and Δ\Delta are judgmentally equal contexts in the crisp mode;

  • ΓΔctxat𝒸\Gamma \equiv \Delta \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c} which says that Γ\Gamma and Δ\Delta are judgmentally equal contexts in the cohesive mode;

The original papers on multimodal type theory use the symbol @ instead of at\mathrm{at} but it doesn’t seem to be possible to put @ inside of latex math mode on the nLab, whether directly or inside the mathrm command.

Then we have the rules for the context locks of the modalities of cohesive homotopy type theory:

Γctxat𝒹Γ,lock p !ctxat𝒸Γctxat𝒸Γ,lock p *ctxat𝒹Γctxat𝒹Γ,lock p *ctxat𝒸Γctxat𝒸Γ,lock p !ctxat𝒹\frac{\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d}}{\Gamma, \mathrm{lock}_{p_!} \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c}} \qquad \frac{\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c}}{\Gamma, \mathrm{lock}_{p^*} \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d}} \qquad \frac{\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d}}{\Gamma, \mathrm{lock}_{p_*} \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c}} \qquad \frac{\Gamma \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{c}}{\Gamma, \mathrm{lock}_{p^!} \; \mathrm{ctx} \; \mathrm{at} \; \mathcal{d}}

The original papers also used a lock symbol that the author does not know how to replicate on the nLab.

(…)

(Kolomatskaia & Shulman 2023 might also be useful here in defining the type theory)

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.

Cohomology

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 \,.

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.

(…)

References

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

was given in

following

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

See also broader discussion in:

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:

following a general pattern for modal type theory laid out in

with exposition in:

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:

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

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

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

Exposition in:

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

For parametricity in cohesive homotopy type theory:

The development of cohesive homotopy type theory as a multimodal type theory uses material from

Last revised on August 21, 2024 at 11:11:51. See the history of this page for a list of all contributions to it.