# Spahn internal formulation of cohesion

category: cohesion

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

For generalities on the formulation of Ho TT in Coq see HoTT-Coq - references.

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

For a blog comment on the internal formulation of cohesion, see Mike Shulman

• internalizing the external - the joy of codiscreteness, ncafé

• discreteness, concreteness, fibrations, and scones, ncafé

## Notation

We assume that

$(\Pi\dashv Disc\dashv \Gamma\dashv co Disc):\infty Grpd\stackrel{co Disc}{\hookrightarrow}H$

is an adjoint quadruple, where we assume that $\Pi$ preserves finite products and $Disc$ and $co Disc$ are full and faithful.

$(\mathbf{\Pi}\dashv \flat\dashv\sharp):=(Disc \Pi \dashv Disc \Gamma\dashv co Disc \Gamma):H\to H$

## 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}$

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

2. a morphism $\mathbf{\flat} X \to X$ with $\mathbf{\flat} X \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$;

3. 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

1. $\mathbf{H}(\mathbf{\Pi}X , Y) \stackrel{\simeq}{\to} \mathbf{H}(X,Y)$;

2. $\mathbf{H}(Y, \mathbf{\flat}X) \stackrel{\simeq}{\to} \mathbf{H}(Y,X)$;

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

4. $# (\flat X \to X)$;

5. $\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

Assuming that the internal language $I$ of a topos $H$ is homotopy type theory the goal is to write some coq code which type-checks iff $H$ is cohesive.

One can write down easily some coq code which is satisfied for all types in $I$ iff $H$ is cohesive (this is done below).

However homotopy type theory is a dependent type theory? and hence contains also dependent types. So it is a different and more interesting game to strictify rules and try to write some coq code which is satisfied for all dependent types in $I$ iff $H$ is cohesive. (In particular if one has solved the stricter problem by identifying a type $A$ with the dependent type $id_A$ one obtains also a solution to the easier one.)

The approach taken below departs from the notion of reflective subfibration.

###### Definition

A reflective subfibration is defined to be a reflective subcategory of each slice category, such that pullback preserves the subcategories and commutes with the reflector.

### Subtopos

#### Reflective subfibration

This section comments on the code ReflectiveSubfibration.v.

It codes the Ho CT axiom that

$(\Gamma\dashv \co Disc):\infty Grpd\to H$

exhibits the codiscrete objects as reflective subcategory of $H$.

###### Definition

A reflective subfibration is defined to be a reflective subcategory of each slice category, such that pullback preserves the subcategories and commutes with the reflector.

The following typeclass rsf axiomatizes the notion of reflective subfibration in coq:

###### Definition

Class rsf (in_rsc : Type -> Type) := {

in_rsc_prop : forall X, is_prop (in_rsc X)

; reflect : Type -> Type

; reflect_in_rsc : forall X, in_rsc (reflect X)

; to_reflect : forall X, X -> reflect X

; reflect_is_reflection : forall X Y, in_rsc Y ->

 is_equiv (fun f: reflect X -> Y => f o to_reflect X)

}.

##### For plain types

The following axioms characterize in type theoretical language the relations between objects of a reflective subcategory by means of the endofunctor

$\sharp= co Disc \Gamma: H\to H$
1. $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).

2. $A:Type\dashv \sharp A:Type.$ This says that for any $A$, we have another type $\sharp A$ (its reflection into the subcategory).

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

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

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

In category theory this means that

$\array{ \sharp P(x)&\rightarrow &\sharp P \\ \downarrow&&\downarrow \\ *&\xrightarrow{x}&A }$

is a pullback and the right arrow is a fibration. The operation $\sharp$ commutes with pullbacks and gives an operation on every overcategory $H/A$ . There are axioms expressing the requirement that $\sharp$ is a reflection.

### Relation to factorization systems

###### Theorem

(1) The following statements are equivalent:

• $(E,M)$ is a reflective factorization system in $H$.

• There is a reflective subcategory $C\hookrightarrow H$ with reflector $\sharp$, $E$ is the class of morphisms whose $\sharp$-image is invertible in $C$, and $C=M/1$.

• $(E,M)$ is a factorization system and $E$ satisfies 2-out -of-3.

• $(E,M)$ is a factorization system and $M$ is the class of fibrant morphisms $P\to A$ which as dependent types $x:A\dashv P(x): Type$ satisfy $forall\, x \,in Rsc(P(x))$.

• For every $H$-morphism $f:A\to B$ satisfying: $\sharp A$ and $\sharp B$ are contractible, also for all $b$ we have $\sharp \, hFiber(f,b)$ is contractible.

$is Contr(\sharp A),is Contr(\sharp B), f:A\to B, b:B\vdash is Contr (\sharp h Fiber(f,b))$

(2) The following statements are equivalent:

• $(E,M)$ is a factorization system in $H$.

• The class $(E,M)^\times:=\{M/x|x\in H,\M/x\hookrightarrow H/x\,is.refl,\,refl.fact\}$ is pullback-stable where $refl.fact$ means that each reflection is defined by $(E,M)$-factorization.

• $(C.x\subseteq H/x)_{x\in H}$ is a pullback-stable system of reflective subcategories of slices of $H$, and for every $x$ the class of objects of $C.x$ is closed under composition.

• The class of types $B$ satisfying $in Rsc (B)$ is closed under dependent sums.

$in Rsc(A), forall \, x,in Rsc(P(x))\vdash in Rsc (\sum_{x:A} P(x))$

(3) The following statements are equivalent:

• $(C.x\subseteq H/x)_{x\in H}$ is a pullback-stable system of reflective subcategories of slices of $H$, for every $x$ the class of objects of $C.x$ is closed under composition, and all reflectors commute with pullbacks.

• The (by (2)) to $(C.x\subseteq H/x)_{x\in H}$ corresponding factorization system $(E,M)$ is pullback stable.

github

#### Lex-reflective subcategory

###### Theorem

Let $C$ be a ccc. Let $I\hookrightarrow C$ be a reflective subcategory.

Then $I$ is an exponential ideal iff the reflector preserves finite products.

github

github

### Local topos

$H$ being local means that we have a geometric morphism with extra right adjoint

github

### Cohesive topos

(Discrete objects are reflectively- and coreflectively embedded.)

github

• Mike Shulman, Discreteness, Concreteness, Fibrations, and Scones, blog

• Mike Shulman, Internalizing the External, or The Joys of Codiscreteness, blog

• Mike Shulman, Reflective Subfibrations, Factorization Systems, and Stable Units, blog