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 [[nLab:Urs Schreiber]], _[[schreiber:differential cohomology in a cohesive topos]]_ ## The Ho CT-axioms of cohesion +-- {: .num_theorem} ###### theorem For $Disc : \mathbf{B} \hookrightarrow \mathbf{H}$ a [[nLab:sub-(∞,1)-category]], the inclusion extends to an [[nLab: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}$; 1. a morphism $\mathbf{\flat} X \to X$ with $\mathbf{\flat} X \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$; 1. 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)$; 1. $\mathbf{H}(Y, \mathbf{\flat}X) \stackrel{\simeq}{\to} \mathbf{H}(Y,X)$; 1. $\mathbf{H}(# X , \tilde Y) \stackrel{\simeq}{\to} \mathbf{H}(X,\tilde Y)$; 1. $# (\flat X \to X)$; 1. $\flat (X \to # X)$ are [[nLab:equivalence in an (infinity,1)-category|equivalences]] (the first three of [[nLab:∞-groupoids]] the last two in $\mathbf{H}$). Moreover, if $\mathbf{H}$ is a [[nLab:cartesian closed category]], then $\Pi$ preserves finite products precisely if the $Disc$-inclusion is an [[nLab:exponential ideal]]. =-- The last statement follows from the $(\infty,1)$-category analog of the discussion [here](http://ncatlab.org/nlab/show/reflective+subcategory#ReflectiveSubcategoriesOfCartesianClosedCategotries). ## Coq This section is on the [[nLab:Coq]] formalization of [[nLab:cohesive (infinity,1)-topos|axiomatic homotopy cohesion]]. It draws from [[nLab:Mike Shulman]], _Internalizing the external, or The Joys of Codiscreteness_ ([blog post](http://golem.ph.utexas.edu/category/2011/11/internalizing_the_external_or.html)). The corresponding Coq-code library is at [[nLab:Mike Shulman]], _[HoTT/Coq/Subcatgeories](https://github.com/mikeshulman/HoTT/tree/master/Coq/Subcategories)_ ### Subtopos #### Reflective subfibration This section comments on the code [ReflectiveSubfibration.v](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/ReflectiveSubfibration.v). ##### For plain types The following axioms characterize in type theoretical language the relations between objects of a reflective subcategory $$A\stackrel{\xleftarrow{\sharp}}{\hookrightarrow} H$$ and objects of the ambient category $H$ wrt. the reflector $\sharp\dashv \iota$: 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). 1. $A:Type\dashv \sharp A:Type.$ This says that for any $A$, we have another type $\sharp A$ (its reflection into the subcategory). 1. $A:Type\dashv in Rsc(\sharp A).$ This says that for any $A$, the type $\sharp A$ is in the subcategory. 1. $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). 1. $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. #### Stable factorization system [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/StableFactorizationSystem.v) #### Lex-reflective subcategory [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/LexReflectiveSubcategory.v) ### Lex-reflective subcategory of codiscrete objects [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/Codiscrete.v) ### Local topos [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/LocalTopos.v) ### Cohesive topos [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/CohesiveTopos.v)