Spahn infinitesimal cohesive type theory (Rev #2)

Prerequisites

internal formulation of cohesion

Notation

The adjoint triple induced by the original adjoint quadruple defining infinitesimal cohesion is denoted

(RedΠ inf):H thH th(Red\dashv \Pi_inf\dashv\flat):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 18:42:30 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.