Spahn infinitesimal cohesive type theory (Rev #3)

Prerequisites

internal formulation of cohesion

Notation

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

(RedΠ inf dR):H thH th(\mathbf{Red}\dashv \mathbf{\Pi_inf}\dashv\flat_dR):H_th\to H_th

Infinitesimal cohesion

Let HH, H thH_th be cohesive toposes. An adjoint triple

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

is said to exhibit an infinitesimal cohesion if i !i_! is full, faithful and preserves the terminal object.

Remark

(1) It follows from the definition that also i *i_* is full and faithful.

(2) (i *i *)(i^*\dashv i_*) is a (geometric) morphism of toposes over Grpd\infty Grpd. This means that

H (i *i *) H th Γ Γ Grpd \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 *i !)(i_* \dashv i^!)

H th (i *i !) H Γ Γ Grpd. \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.