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

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

Prerequisites Comparing cohesion with infinitesimal cohesion

~~internal formulation of cohesion~~An adjoint quadruple

~~Notation~~

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

~~The~~ exhibits ~~adjoint~~ ~~triple~~ ~~induced~~ by ~~the~~ ~~original~~ ~~adjoint~~ ~~quadruple~~ ~~$(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~~

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

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^!$ .)

~~Infinitesimal cohesion~~

The adjoint triples induced by these adjoint quadruples we denote by

~~Let $H$ , $H_th$ be cohesive toposes. An adjoint triple~~

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)$

~~$(i_!\dashv i^*\dashv i_*):H\stackrel{i_*}{\to}H_th$~~

Internal formulation of cohesion

is The ~~said~~ encoding to of cohesion in Ho TT proceeds in the following steps~~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 } \,.$

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

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