Todd Trimble
Cartesian closure of internal categories

We give a simple proof of the following result.


Let E\mathbf{E} be a finitely complete cartesian closed category. Then the category Cat(E)Cat(\mathbf{E}) of internal categories in EE is also finitely complete and cartesian closed.


First suppose E\mathbf{E} is finitely complete. Then the category of directed graphs E \mathbf{E}^{\bullet \stackrel{\to}{\to} \bullet} is also finitely complete, and since Cat(E)Cat(\mathbf{E}) is monadic over E \mathbf{E}^{\bullet \stackrel{\to}{\to} \bullet}, it follows that Cat(E)Cat(\mathbf{E}) is also finitely complete.

Now suppose that E\mathbf{E} is finitely complete and cartesian closed. Let Δ 3\Delta_3 denote the category of nonempty ordinals up to and including the ordinal with 4 elements. We have a full and faithful embedding

N:Cat(E)E Δ 3 opN \colon Cat(\mathbf{E}) \to \mathbf{E}^{\Delta_3^{op}}

where the codomain category is cartesian closed. Indeed, the exponential of two objects FF, GG in E Δ 3 op\mathbf{E}^{\Delta_3^{op}} may be computed as an E\mathbf{E}-enriched end

G F(m)= n f:nmG(n) F(n)G^F(m) = \int_n \prod_{f \colon n \to m} G(n)^{F(n)}

when evaluated at mOb(E Δ 3 op)m \in Ob(\mathbf{E}^{\Delta_3^{op}}), as is easily checked (see for instance here); note that this end is a finite limit diagram since Δ 3\Delta_3 is finite.

If CC, DD are internal categories in E\mathbf{E}, seen as functors Δ 3 opE\Delta_3^{op} \to \mathbf{E}, the exponential NC NDN C^{N D} defines the exponential in Cat(E)Cat(\mathbf{E}). To see this, it suffices to check that NC NDN C^{N D}, as defined by the end formula above, is a category BB, i.e., is in the essential image of the nerve functor. For in that case, we have natural isomorphisms

F×DCinCat(E) NF×NDN(F×D)NCinE Δ 3 op NFNC NDinE Δ 3 op FBinCat(E) \array{ \arrayopts{\rowlines{solid}} F \times D \to C\;\;\; in\; Cat(\mathbf{E}) \\ N F \times N D \cong N(F \times D) \to N C\;\;\; in\; \mathbf{E}^{\Delta_3^{op}} \\ N F \to N C^{N D}\;\;\; in\; \mathbf{E}^{\Delta_3^{op}} \\ F \to B\;\;\; in \; Cat(\mathbf{E}) }

whence BB satisfies the universal property required of an exponential.

Objects in the essential image of the nerve NN are characterized as functors Δ 3 opE\Delta_3^{op} \to \mathbf{E} which take intervalic joins in Δ 3\Delta_3 to pullbacks in E\mathbf{E}, as given precisely by the Segal conditions. The remainder of the proof is then finished by the following lemma.


If C:Δ 3 opEC \colon \Delta_3^{op} \to \mathbf{E} satisfies the Segal conditions and X:Δ 3 opEX \colon \Delta_3^{op} \to \mathbf{E} is any functor, then C XC^X also satisfies the Segal conditions.


For any XX we have the formula

C X(m)= kHom(Xk, f:nk g:nmC(n)).C^X(m) = \int_k Hom(X k, \prod_{f \colon n \to k} \prod_{g \colon n \to m} C(n)).

Since the enriched end and the internal hom-functor Hom(Xk,)Hom(X k, -) both preserve pullbacks, we are reduced to checking that

  • If CC satisfies the Segal conditions, then so does
    f:nk g:nmC(n)\prod_{f \colon n \to k} \prod_{g \colon n \to m} C(n)

    as a functor Δ 3 opE\Delta_3^{op} \to \mathbf{E} in the argument mm (for each fixed kk).

Note that the displayed statement is a proposition in the language of finitely complete categories (i.e., in finitary essentially algebraic logic). Since hom-functors E(e,):ESet\mathbf{E}(e, -) \colon \mathbf{E} \to Set jointly preserve and reflect the validity of such propositions, it suffices to prove it for the case where E=Set\mathbf{E} = Set. But this is classical elementary category theory; it says precisely that if CC is a small (ordinary) category, then the usual functor categories C 2C^{\mathbf{2}}, C 3C^{\mathbf{3}} are equivalently described by exponentials of (truncated) simplicial sets. This completes the proof.

Revised on October 28, 2016 at 20:54:41 by Todd Trimble