Spahn internal formulation of cohesion (Rev #2)

The axioms

theorem

For $Disc : \mathbf{B} \hookrightarrow \mathbf{H}$ a sub-(∞,1)-category, the inclusion extends to an adjoint quadruple of the form

\mathbf{H} \stackrel{\overset{\Pi}{\to}}{\stackrel{\overset{Disc}{\hookleftarrow}}{\stackrel{\overset{\Gamma}{\to}}{\underset{coDisc}{\hookleftarrow}}}} \mathbf{B}

precisely if there exists for each object $X \in \mathbf{H}$

a morphism $X \to \mathbf{\Pi}(X)$ with $\mathbf{\Pi}(X) \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$ ;
a morphism $\mathbf{\flat} X \to X$ with $\mathbf{\flat} X \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$ ;
a morphism $X \to #X$ with $# X \in \mathbf{B} \stackrel{coDisc}{\hookrightarrow} \mathbf{H}$

such that for all $Y \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$ and $\tilde Y \in \mathbf{B} \stackrel{coDisc}{\hookrightarrow} \mathbf{H}$ the induced morphisms

$\mathbf{H}(\mathbf{\Pi}X , Y) \stackrel{\simeq}{\to} \mathbf{H}(X,Y)$ ;
$\mathbf{H}(Y, \mathbf{\flat}X) \stackrel{\simeq}{\to} \mathbf{H}(Y,X)$ ;
$\mathbf{H}(# X , \tilde Y) \stackrel{\simeq}{\to} \mathbf{H}(X,\tilde Y)$ ;
$# (\flat X \to X)$ ;
$\flat (X \to # X)$

are equivalences (the first three of ∞-groupoids the last two in $\mathbf{H}$ ).

Moreover, if $\mathbf{H}$ is a cartesian closed category, then $\Pi$ preserves finite products precisely if the $Disc$ -inclusion is an exponential ideal.

The last statement follows from the $(\infty,1)$ -category analog of the discussion here.

Coq

Subtopos

Reflective subfibration

github

$A:Type\vdash inRsc(A):Prop.$ This says that for any type $A$ , we have a proposition $inRsc(A)$ (expressing the assertion that $A$ is in our putative reflective subcategory).
A:Type\dashv \sharp A:Type. $This says that for any$ A $, we have another type \sharp A$ (its reflection into the subcategory).

$A:Type\dashv inRsc(\sharp A).$ This says that for any $A$ , the type $\sharp A$ is in the subcategory.

$A:Type\dashv \eta_A:A\to \sharp A$ . This says that for any $A$ , we have a map $\eta_A:A\to \sharp A$ .

$A,B:Type,inRsc(B)\dashv isEquiv(\lambda g.g\circ\eta A)$ . This says that for any types A and B, where B is in the subcategory, precomposing with $\eta A$ yields an equivalence between $B\sharp A$ and $BA$ .

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

Spahn internal formulation of cohesion (Rev #2)

The axioms

theorem

Coq

Subtopos

Reflective subfibration

Stable factorization system

Lex-reflective subcategory

Lex-reflective subcategory of codiscrete objects

Local topos

Cohesive topos