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) #### 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)