Spahn internal formulation of cohesion (Rev #2, changes)

theorem

For $Disc : \mathbf{B} \hookrightarrow \mathbf{H}$ a sub-(∞,1)-category, the inclusion extends to an adjoint quadruple of the form

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.