Spahn infinitesimal cohesive type theory

Comparing cohesion with infinitesimal cohesion

An adjoint quadruple

(i_!\dashv i^* \dashv i_*\dashv i^!)

exhibits

cohesion, if $i^*$ and $i^!$ are full, faithful and $i_!$ preserves finite products
infinitesimal cohesion, if $i_!$ and $i_*$ are full, faithful and $i_!$ preserves the terminal object. (In some cases we do not care about $i^!$ .)

The adjoint triples induced by these adjoint quadruples we denote by

in the cohesive case by $(\mathbf{\Pi}\dashv \flat\dashv\sharp)$
in the infinitesimal cohesive case by $(\mathbf{Red}\dashv\mathbf{\Pi}_inf\dashv \flat_dR)$

Internal formulation of cohesion

The encoding of cohesion in Ho TT proceeds in the following steps

(1a) $(i_!\dashv i^*)$ (resp. $\sharp$ ) determines a reflective subcategory. In “independent” type theory, the axioms for this are displayed in internal formulation of cohesion. However if we consider these axioms in Ho TT (which is a dependent type theory) these axioms do not define a reflective subcategory but a reflective subfibration?. This means that we need a translation of the notion of reflective subfibration back to that of reflective subcategory. This translation is:

(1b)

Internal formulation of infinitesimal cohesion

We proceed by encoding the following partial notions:

$(i_!\dashv i^*)$ (resp. $\mathbf{Red}$ ) determines a coreflective subcategory.
$i_!$ preserves the terminal object.
$(i^*\dashv i_*)$ (resp. $\mathbf{\Pi}_inf$ ) determines a reflective subcategory
$(i_*\dashv i^!)$ (resp. $\flat_dR$ ) determines a coreflective subcategory. (In some cases we do not care about this last axiom.)

Formulation in Coq

Properties of infinitesimal cohesion

Remark

(1) It follows from the definition that also $i_*$ is full and faithful.

(2) $(i^*\dashv i_*)$ is a (geometric) morphism of toposes over $\infty Grpd$ . This means that

\array{ \mathbf{H} && \stackrel{(i^* \dashv i_*)}{\to} && \mathbf{H}_{th} \\ & {}_{\mathllap{\Gamma}}\searrow && \swarrow_{\mathrlap{\Gamma}} \\ && \infty Grpd }

commutes.

(3) The same holds for $(i_* \dashv i^!)$

\array{ \mathbf{H}_{th} && \stackrel{(i_* \dashv i^!)}{\to} && \mathbf{H} \\ & {}_{\mathllap{\Gamma}}\searrow && \swarrow_{\mathrlap{\Gamma}} \\ && \infty Grpd } \,.