## Prerequisites [[internal formulation of cohesion]] ## Infinitesimal cohesion Let $H$, $H_th$ be cohesive toposes. An adjoint triple $$(i_!\dashv i^*\dashv i_*):H\stackrel{i_*}{\to}H_th$$ is said to *exhibit an infinitesimal cohesion* if $i_!$ is full, faithful and preserves the terminal object. +-- {: .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 } \,. $$ =-- ## Formulation in Coq