The n-Category Café

Now how do we describe a reflective or coreflective subcategory internally? In the obvious approach, we just say what it means to belong to the subcategory, plus have an operation on the types which serves as the reflector/coreflector, together with a unit/counit satisfying a suitable universal property. In the reflective case, this means we have something like the following axioms.

• $A\colon Type \vdash inRsc(A) \colon 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\colon Type \vdash \sharp A \colon Type$. This says that for any $A$, we have another type $\sharp A$ (its reflection into the subcategory).
• $A \colon Type \vdash inRsc(\sharp A)$. This says that for any $A$, the type $\sharp A$ is in the subcategory.
• $A \colon Type \vdash \eta_A \colon A \to \sharp A$. This says that for any $A$, we have a map $\eta_A \colon A \to \sharp A$.
• $A,B \colon Type, inRsc(B) \vdash 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 $B^A$.

However, assuming that our type theory has dependent types, an operation on types specified in the internal logic in this way actually gives us more than merely an operation on objects of $H$ (which is what we had in mind). This is because any operation we have in type theory can automatically be applied in any context. Hence, not only can we say that for every type $A$, we have a type $\sharp A$, we can also say that for any dependent type $$x\colon A \vdash P(x) \colon Type$$ we have another dependent type $$x\colon A \vdash \sharp P(x) \colon Type.$$ Since dependent types over $A$ represent objects in the slice category $H/A$, a type-theoretic operation $\sharp$ actually gives us an operation on every slice category of $H$. This should make sense in terms of the vague description of the internal logic I gave above, once you realize that if a “generalized element of $A$ at stage $U$” means a morphism $U\to A$, then a “generalized object of the category at stage $U$” can only mean an object of the slice category $H/U$.

Moreover, this operation on slice categories commutes with pullback, since the pullback of $\sharp P$ along $f\colon B\to A$ and the $\sharp$-image of the pullback of $P$ along $f$ are both represented by the same dependent type: $y \colon B \vdash \sharp P(f(y)) \colon Type$. If we additionally add axioms which appear to say that this operation a reflection or coreflection (as I did above for a reflection), then we are actually describing a reflective or coreflective subcategory of every slice category, for which the (co)reflector commutes with pullback – a (co)reflective subfibration of the codomain fibration.

So how can we eliminate this extra data and get back to talking about a reflective or coreflective subcategory of $H$ itself? In the coreflective case, we’re pretty sunk (I’ll get back to that case later), but in the reflective case, there is a close relationship between reflective subcategories and reflective subfibrations.

1. Every reflective subcategory (subject to certain adjoint-functor-theorem-y conditions) gives rise to a factorization system $(E,M)$, in which $E$ is the class of maps inverted by the reflector $\sharp$, and the reflective subcategory is identified with $M/1$. The factorization systems which arise from reflective subcategories in this way are precisely those for which $E$ satisfies two-out-of-three (in which case, of course, the reflective subcategory is the localization at $E$); these are called reflective factorization systems.

2. Every factorization system $(E,M)$ gives rise to a pullback-stable system of reflective subcategories of slice categories: the subcategory of $H/x$ is $M/x$, with the $(E,M)$-factorization being the reflection. A pullback-stable system of reflective subcategories $C^x \subseteq H/x$ arises from a factorization system in this way precisely when $M$, the class of morphisms $f\colon x\to y$ which are objects of $C^x$, is closed under composition. The reflectors also commute with pullback (giving a reflective subfibration) precisely when the factorization system itself is pullback-stable.

3. A reflective factorization system is stable precisely when its corresponding reflective subcategory has a left-exact reflector.

A couple of good references to learn about this stuff are given at the bottom of this page. Thus, we have a diagram of inclusions: $$\array{ \text{reflective subcategories} & \to & \text{factorization systems} & \to & \text{systems of reflective subcategories}\\ \uparrow & & \uparrow & & \uparrow\\ \text{lex-reflective subcategories}& \to & \text{stable factorization systems} & \to & \text{reflective subfibrations} }$$ Recall that the naive internal axioms, which look as though they are describing a reflective subcategory, actually describe a reflective subfibration. Thus, we can augment them to actually describe a lex-reflective subcategory by imposing further axioms ensuring that $M$ is closed under composition and that $E$ satisfies two-out-of-three.

It turns out that internally, the class $M$ consists of the morphisms $P\to A$ which represent dependent types $x\colon A \vdash P(x) \colon Type$ for which $\forall x, inRsc(P(x))$. One can prove from this that $M$ will be closed under composition just when, internally, the types for which $inRsc(B)$ are closed under dependent sums:

$$inRsc(A), \forall x. inRsc(P(x)) \vdash inRsc \left(\sum_{x\colon A} P(x)\right)$$

Similarly, $E$ can be characterized internally as the morphisms which represent dependent types $x\colon A \vdash P(x) \colon Type$ for which each $\sharp P(x)$ is contractible. One can prove from this that $E$ satisfies two-out-of-three just when, internally, for any map $f\colon A\to B$ where $\sharp A$ and $\sharp B$ are contractible, so is the $\sharp$ of all homotopy fibers of $f$.

$$isContr(\sharp A), isContr(\sharp B), f\colon A\to B, b\colon B \vdash isContr(\sharp hFiber(f,b))$$

This last condition is a special case of saying that $\sharp$ preserves pullbacks, and from it one can prove internally that $\sharp$ preserves all pullbacks – that is, the reflector is lex. In fact, though, even without these latter two conditions, there is a certain amount of lex-ness even to the notion of reflective subfibration. For since the reflector commutes with pullback, so do their right adjoints: the inclusions of the fiberwise subcategories and dependent products. This implies in particular that $M/1$ is an exponential ideal, and hence $\sharp$ must preserve finite products.

The closure of the subcategory under dependent sums is a somewhat more mysterious condition. However, it admits a very pleasing reformulation. Notice that one consequence of the axiom asserting the universal property of $\eta_A$ is that we can factor through it:

• $f\colon A\to B, inRsc(B) \vdash fact(f)\colon \sharp A \to B$. This says that if $B$ is in the subcategory and $f\colon A\to B$, then we have another map $fact(f)\colon \sharp A \to B$.
• $f\colon A\to B, inRsc(B), a\colon A \vdash fact(f)(\eta_A(a)) = f$. This says that for $A,B$ and $f$ as above, and any $a\colon A$, we have $fact(f)(\eta_A(a)) = f$.

This looks a lot like the “elimination rule” of an inductively defined type, a common notion in type theory. In general, when a type $T$ is inductively defined by certain constructors, it means that we have various ways to construct elements of $T$ (perhaps taking as input other elements of $T$), and moreover if we have any other type $B$ together with similar ways to construct elements of $B$, there is a specified map from $T$ to $B$ preserving the constructors. For instance, the natural numbers are inductively defined by two constructors $0\colon \mathbb{N}$ and $s\colon \mathbb{N}\to \mathbb{N}$.

Here, we seem to be sort-of saying that $\sharp A$ is inductively defined by $\eta_A\colon A\to \sharp A$, together with a certain vague “sharpness”. In particular, it has an eliminator saying that if $B$ has a similar constructor $f\colon A\to B$ together with the same sort of “sharpness” (that is, $inRsc(B)$), then we have a specified map $fact(f)\colon \sharp A\to B$ preserving the constructor $\eta_A$ (evidently “preserving sharpness” is a vacuous condition, which makes sense since our subcategory is full).

However, in dependent type theory, inductive types generally also come with dependent eliminators, in which the target type $B$ is allowed to depend on the inductive type $T$. For instance, for the natural numbers this eliminator says that given a dependent type $n\colon \mathbb{N}\vdash B(n) \colon Type$ together with an element $z_B\colon B(0)$ and for every $n$ an operation $s_B \colon B(n) \to B(s(n))$, we have a specified section $f \colon \forall n, B(n)$ such that $f(0)= z_B$ and $s_B(f(n)) = f(s(n))$. One value of the dependent eliminators is that they allow us to prove uniqueness (up to equality, i.e. paths in homotopy theory) of the morphisms specified by the non-dependent eliminator, by using the dependent eliminator into an equality/path type.

A natural dependent eliminator for $\sharp$ would be the following. Suppose $a\colon \sharp A \vdash B(a)$ is a type dependent on $\sharp A$, suppose we have a section $f\colon \forall a\colon A, B(\eta_A(a))$ over $A$, and suppose that $\forall x\colon \sharp A, inRsc(B(x))$. Then we have a specified section $fact(f)\colon \forall x\colon \sharp A, B(x)$, such that $\fact(f)(\eta_A(a)) = f(a)$ for all $a\colon A$.

Here’s the lovely fact: a reflective subfibration $\sharp$ has a dependent eliminator if and only if the $inRsc$ objects are closed under dependent sums, i.e. it is a factorization system. If we have closure under sums, then we can use the non-dependent eliminator to define a map $A\to \sum_{x\colon \sharp A} B(x)$ and nudge it so it becomes a section of $B$; while conversely we can define an inverse to $\eta_{\Sigma_x B(x)}$ using the dependent eliminator. Moreover, if we assume that the subcategory is closed under equality/path types, then the dependent eliminator implies not just the non-dependent eliminator (which is obvious) but also its universal property (by eliminating into an equality type).

This gives a very type-theoretic style of thinking about $\sharp$, which is also very convenient for proving things about sharped objects. We can write convenient tactics in Coq which automatically apply the dependent eliminator and its computation rules to reduce everything to statements about unsharped objects. In a sense, it’s saying that we have a higher-categorical sort of modality: one which acts on objects as well as on propositions. This shouldn’t be too surprising; we know that lex-reflective subcategories of a 1-topos are equivalent to Lawvere-Tierney topologies, which are a traditional sort of modality which acts on propositions. In homotopy type theory, we need to use higher modalities which act on objects because not every sub-$(\infty,1)$-topos is a topological localization.

I hope that the foregoing has convinced you that codiscrete objects admit a very nice and convenient axiomatization in the internal logic. Unfortunately, discrete objects don’t admit nearly so nice a description, because the internal logic doesn’t let us dualize the slice categories into co-slices when we want to dualize reflectiveness into coreflectiveness. I don’t know of any general way to construct a coreflective subfibration.

However, if we have codiscrete objects, then they give us a solution for dealing with the discrete objects! Namely, we already have the category $S$ sitting inside $H$ as the codiscrete objects, with the functor $U\colon H\to S$ represented by the reflector $\sharp$. Thus, we can talk “in $S$” “about $H$” and still remain inside $H$, if we do all of our talking inside the codiscrete objects.

The main player in this approach is $\sharp Type$. Here $Type$ is the (or, rather, a) type of types, which represents an object classifier in category theory. You can think of it as like a Grothendieck universe of sorts; but remember that we want it to satisfy the univalence axiom. Thus, $\sharp Type$ is the object of $S$ underlying $Type$ – which we can think of as the “external space of objects of $H$” – included back into $H$ as a codiscrete object. The functoriality of $\sharp$ (and the fact that it preserves products) means that any operation on types, which is described in type theory by a function on $Type$, gives rise to a corresponding “externalized” function on $\sharp Type$. For instance, the internal-hom, which takes two types A and B and gives the function-type A -> B, is represented by a function $Type \;\times\; Type \to Type$, and hence gives us a function $\sharp Type \;\times\; \sharp Type \to \sharp Type$.

Something is still missing, though. The function $\sharp Type \;\times\; \sharp Type \to \sharp Type$ is an externalization of the internal-hom operation, which takes two objects of $H$ and gives us a third object of $H$. However, what we really want (in order to talk about $H$ “externally”) is the external hom, which takes two objects of $H$ and gives us an object of $S$! Thus we need an operation $\sharp Type \to Type$ which “escapes” from the external world, in a sense, and which should be a version of $\sharp$ itself (since the external-hom is $U$ applied to the internal-hom).

Magically, we have just such an operation. Recall that the object classifier $Type$ comes with a universal map $\widetilde{Type} \to Type$, of which every (small) map is a pullback in an essentially unique way. The functor $\sharp$ applied to this gives us a map $\sharp\widetilde{Type} \to \sharp Type$, which therefore has a classifying map $escape \colon \sharp Type \to Type$. It’s an easy exercise in pasting pullback squares, using the fact that $\sharp$ preserves pullbacks, to show that the composite $$Type \xrightarrow{\eta_{Type}} \sharp Type \xrightarrow{escape} Type$$ is equivalent to $\sharp\colon Type \to Type$ itself. Thus, escape really is “a version of sharp”, and it lets us define the external hom $\sharp Type \;\times\; \sharp Type \to Type$ by composing the “externalized internal-hom” with escape.

This works amazingly well. In particular, it allows us to express the coreflector for the discrete objects in terms of an operation $\flat\colon \sharp Type \to \sharp Type$, state its universal property, and prove useful things about it. It’s more cumbersome than working purely internally, of course, but as we get more practice we’ll write more helpful tactics and it will get easier. It’s just as easy to additionally assert that the discrete objects are also reflective, with reflector $\Pi$ that preserves finite products, thereby obtaining the original desired axiomatization of cohesive $(\infty,1)$-toposes. The axiomatization that I’m now satisfied with can be found here.

Let me finish by saying a bit about what we can do if we don’t have codiscrete objects. Remember from last time that there is a universal way to add codiscrete objects, by constructing the scone on a (lex) functor $U\colon H\to S$. Thus, if we want to talk about such a functor using internal logic, we can first construct its scone, which contains $S$ as a lex-reflective subcategory of codiscrete objects.

Moreover, the scone also contains $H$ as a lex-reflective subcategory, and these two subcategories are complementary open and closed subtoposes. (An open subtopos is determined by a subterminal object $P$, and its reflector is $A\mapsto A^P$; the reflector of the complementary closed subtopos takes $A$ to the pushout of the two projections of $A\times P$.) Finally, any topos equipped with a complementary pair of open and closed subtoposes can be obtained as the scone of a functor from the one to the other. Thus, if we axiomatize two lex-reflective subcategories as above and stipulate that they are complementary open and closed subtoposes, we will have an internal logic with which to talk about arbitrary lex functors between toposes. And if we furthermore require that the codiscrete objects (those in the closed subtopos) come with matching discrete ones, this corresponds to asking that $U$ have a lex left adjoint; thus we have an internal language with which to talk about arbitrary geometric morphisms.