Spahn infinitesimal cohesive type theory (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Prerequisites

Notation

The adjoint triple induced by the original adjoint quadruple ~~defining~~ ~~infinitesimal~~ ~~cohesion~~ is ~~denoted~~ $(i_!\dashv i^* \dashv i_*\dashv i^!)$ (where in fact $i^!$ is not used in the basic definition, only in some applications) defining infinitesimal cohesion is denoted by

(Red Red ⊣ Π_{\inf} Π_{\inf} ⊣ ♭ ♭_{dR}) : H_{th} \to H_{th}

~~(Red\dashv~~ (\mathbf{Red}\dashv ~~\Pi_inf\dashv\flat):H_th\to~~ \mathbf{\Pi_inf}\dashv\flat_dR):H_th\to H_th

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.

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

Revision on November 26, 2012 at 20:54:37 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.