category: cohesion ## The axioms +-- {: .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 ### Subtopos #### Reflective subfibration [github](https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/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). $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$. #### 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)