Spahn internal formulation of cohesion (Rev #3, changes)

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

~~The axioms~~

For generalities on the translation Ho CT-Ho TT see dictionary HoCT-HoTT.

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.

For generalities on cohesive toposes see Urs Schreiber, differential cohomology in a cohesive topos

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

The Ho CT-axioms of cohesion

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

This section is on the Coq formalization of axiomatic homotopy cohesion. It draws from Mike Shulman, Internalizing the external, or The Joys of Codiscreteness (blog post). The corresponding Coq-code library is at Mike Shulman, HoTT/Coq/Subcatgeories

Subtopos

Reflective subfibration

~~github~~This section comments on the code ReflectiveSubfibration.v.

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

For plain types

~~$A:Type\dashv inRsc(\sharp A).$~~ The following axioms characterize in type theoretical language the relations between objects of a reflective subcategory ~~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\stackrel{\xleftarrow{\sharp}}{\hookrightarrow} H

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

$A:Type\vdash in Rsc(A):Prop.$ This says that for any type $A$ , we have a proposition $in Rsc(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 in Rsc(\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$ (which we can think of as the unit of the adjunction).
$A,B:Type,inRsc(B)\dashv is Equiv(\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 $B^A$ (which we can think of as the adjunction isomorphism since precomposition $g\mapsto g\circ \eta_A$ with the adjunction-unit assigns the adjunct).

For dependent types

The previous axioms are given for plain types but one can impose them also on dependent types $x:A\dashv P(x):Type$ in that we require

x:A \dashv \sharp P(x):Type.

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

Spahn internal formulation of cohesion (Rev #3, changes)

The axioms

theorem

The Ho CT-axioms of cohesion

theorem

Coq

Subtopos

Reflective subfibration

For plain types

For dependent types

Stable factorization system

Lex-reflective subcategory

Lex-reflective subcategory of codiscrete objects

Local topos

Cohesive topos