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 Urs 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é
discreteness, concreteness, fibrations, and scones, ncafé
We assume that
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
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}$
a morphism $X \to \mathbf{\Pi}(X)$ with $\mathbf{\Pi}(X) \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$;
a morphism $\mathbf{\flat} X \to X$ with $\mathbf{\flat} X \in \mathbf{B} \stackrel{Disc}{\hookrightarrow} \mathbf{H}$;
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
$\mathbf{H}(\mathbf{\Pi}X , Y) \stackrel{\simeq}{\to} \mathbf{H}(X,Y)$;
$\mathbf{H}(Y, \mathbf{\flat}X) \stackrel{\simeq}{\to} \mathbf{H}(Y,X)$;
$\mathbf{H}(# X , \tilde Y) \stackrel{\simeq}{\to} \mathbf{H}(X,\tilde Y)$;
$# (\flat X \to X)$;
$\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.
The last statement follows from the $(\infty,1)$-category analog of the discussion here.
This section is on the Coq formalization of axiomatic homotopy cohesion. It draws from Mike Shulman, Internalizing the external, or The Joys of Codiscreteness (blog post). The corresponding Coq-code library is at Mike Shulman, HoTT/Coq/Subcatgeories
Assuming that the internal language $I$ of a topos $H$ is homotopy type theory the goal is to write some coq code which type-checks iff $H$ is cohesive.
One can write down easily some coq code which is satisfied for all types in $I$ iff $H$ is cohesive (this is done below).
However homotopy type theory is a dependent type theory? and hence contains also dependent types. So it is a different and more interesting game to strictify rules and try to write some coq code which is satisfied for all dependent types in $I$ iff $H$ is cohesive. (In particular if one has solved the stricter problem by identifying a type $A$ with the dependent type $id_A$ one obtains also a solution to the easier one.)
The approach taken below departs from the notion of reflective subfibration.
A reflective subfibration is defined to be a reflective subcategory of each slice category, such that pullback preserves the subcategories and commutes with the reflector.
This section comments on the code ReflectiveSubfibration.v.
It codes the Ho CT axiom that
exhibits the codiscrete objects as reflective subcategory of $H$.
A reflective subfibration is defined to be a reflective subcategory of each slice category, such that pullback preserves the subcategories and commutes with the reflector.
The following typeclass rsf
axiomatizes the notion of reflective subfibration in coq:
Class rsf (in_rsc : Type -> Type) := {
in_rsc_prop : forall X, is_prop (in_rsc X)
; reflect : Type -> Type
; reflect_in_rsc : forall X, in_rsc (reflect X)
; to_reflect : forall X, X -> reflect X
; reflect_is_reflection : forall X Y, in_rsc Y ->
is_equiv (fun f: reflect X -> Y => f o to_reflect X)
}.
The following axioms characterize in type theoretical language the relations between objects of a reflective subcategory by means of the endofunctor
$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).
$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 in Rsc(\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$ (which we can think of as the unit of the adjunction).
$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).
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
In category theory this means that
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.
(1) The following statements are equivalent:
$(E,M)$ is a reflective factorization system in $H$.
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.
$(E,M)$ is a factorization system and $M$ is the class of fibrant morphisms $P\to A$ which as dependent types $x:A\dashv P(x): Type$ satisfy $forall\, x \,in Rsc(P(x))$.
For every $H$-morphism $f:A\to B$ satisfying: $\sharp A$ and $\sharp B$ are contractible, also for all $b$ we have $\sharp \, hFiber(f,b)$ is contractible.
(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.refl,\,refl.fact\}$ is pullback-stable where $refl.fact$ means that each reflection is defined by $(E,M)$-factorization.
$(C.x\subseteq H/x)_{x\in H}$ is a pullback-stable system of reflective subcategories of slices of $H$, and for every $x$ the class of objects of $C.x$ is closed under composition.
The class of types $B$ satisfying $in Rsc (B)$ is closed under dependent sums.
(3) The following statements are equivalent:
$(C.x\subseteq H/x)_{x\in H}$ is a pullback-stable system of reflective subcategories of slices of $H$, for every $x$ the class of objects of $C.x$ is closed under composition, and all reflectors commute with pullbacks.
The (by (2)) to $(C.x\subseteq H/x)_{x\in H}$ corresponding factorization system $(E,M)$ is pullback stable.
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.
$H$ being local means that we have a geometric morphism with extra right adjoint
(Discrete objects are reflectively- and coreflectively embedded.)
Last revised on December 4, 2012 at 23:18:34. See the history of this page for a list of all contributions to it.