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]]_ For a blog comment on the internal formulation of cohesion, see Mike Shulman * internalizing the external - the joy of codiscreteness, [ncafé](http://golem.ph.utexas.edu/category/2011/11/internalizing_the_external_or.html) * discreteness, concreteness, fibrations, and scones, [ncafé](http://golem.ph.utexas.edu/category/2011/11/discreteness_concreteness_fibr.html) ## 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. This adjoint quadruple gives rise to an adjoint triple $$(\mathbf{\Pi}\dashv \flat\dashv\sharp):=(Disc \Pi \dashv Disc \Gamma\dashv co Disc \Gamma):H\to H$$ ## 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). It codes the axiom that $$(\Gamma\dashv \co Disc):\infty Grpd\to H$$ exhibits the codiscrete objects as reflective subcategory of $H$. ##### 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). 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. ### Relation to factorization systems (1) The following statements are equivalent: * $(E,M)$ is a *reflective factorization system*. * 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. (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\,reflective,\,fact.refl\}$ is pullback-stable where $fact.refl$ means that each reflection is given by $(E,M)$-factorization. * Here #### Stable factorization system [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/StableFactorizationSystem.v) #### Lex-reflective subcategory +-- {: .num_lemma} ###### 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](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 $H$ being local means that we have a geometric morphism with extra right adjoint [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/LocalTopos.v) ### Cohesive topos (Discrete objects are reflectively- and coreflectively embedded.) [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/CohesiveTopos.v) ## References * Mike Shulman, Discreteness, Concreteness, Fibrations, and Scones, [blog](http://golem.ph.utexas.edu/category/2011/11/discreteness_concreteness_fibr.html) * Mike Shulman, Internalizing the External, or The Joys of Codiscreteness, [blog](http://golem.ph.utexas.edu/category/2011/11/internalizing_the_external_or.html) * Mike Shulman, Reflective Subfibrations, Factorization Systems, and Stable Units, [blog](http://golem.ph.utexas.edu/category/2011/12/reflective_subfibrations_facto.html)