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:

1. $(i_!\dashv i^*)$ (resp. $\mathbf{Red}$) determines a coreflective subcategory.

2. $i_!$ preserves the terminal object.

3. $(i^*\dashv i_*)$ (resp. $\mathbf{\Pi}_inf$) determines a reflective subcategory

4. $(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 } \,.$$