## 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|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. 1. $i_!$ preserves the terminal object. 1. $(i^*\dashv i_*)$ (resp. $\mathbf{\Pi}_inf$) determines a reflective subcategory 1. $(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 +-- {: .num_lemma} ###### 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 } \,. $$ =--