January 2, 2001

Choose a universe V. and a universe U such that V ∈ U. Let Fcc be the category of finitely complete U-small categories with functors preserving finite limits as arrows. An internal category in a finitely complete category C is an object H of C and arrows d_{0}, d_{1}: H → H and comp: H ×_{H} H → H — where H ×_{H} H is the pullback

[figure: H ×_{H} H; snd; H; H; fst; d_{1}; H; d_{0}]

of d_{1} and d_{0} — such that the following diagrams commute:

H  H

(C1)  (C2)

[figure: H; d_{0}; d_{0}; H; d_{1}; H; d_{1}; d_{1}; H; d_{0}]

[figure: H; ⟨id_{H}, d_{1}⟩_{H}; H ×_{H} H; ⟨d_{0}, id_{H}⟩_{H}; H]

(C3)

H comp = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =

[figure: H; fst; H ×_{H} H; snd; H]

(C4)

[figure: H; d_{0}; d_{0}; H; comp; d_{1}; H; d_{1}]

(C5) H ×_{H} H ×_{H} H \overline{\begin{matrix}id_{H} ×_{H} comp \\  \end{matrix}}H ×_{H} H

[figure: H ×_{H} H; comp ×_{H} id_{H}; comp; H; comp]

An internal functor from an internal category (H, d_{0}, d_{1}, comp) in C to an internal category (H′, d′_{0}, d′_{1}, comp′) in C is an arrow F: H → H′ in C such that the following diagrams commute:

H  \overline{F} H′

[figure: (F 1); H; d_{0}; F; H′; d′_{0}]

[figure: H; d_{1}; F; H′; d′_{1}]

H ×_{H} H \overline{\begin{matrix}⟨F ∘ fst, F ∘ snd⟩ & H_{′} \\  \end{matrix}}H′ ×_{H′} H′

(F 2)

[figure: H; comp; F; H′; comp′]

▷ Proposition: Internal categories and internal functors in a finitely complete U-small category C form a U-small category, Int(C). Proof: It clearly follows from the fact that C is U-small that the collections of internal categories in C and internal functors are respectively U-small. We define composition of internal functors in C by composition of the corresponding arrows in C.

• Composition is well-defined: If we have internal functors F: H → H′ and G: H′ → H′′ in C, then certainly G ∘ F is an arrow of C, but we must check that it is an internal functor H → H′′. Preservation of ‘domain’ and ‘codomain’ is an easy diagram-chase:

[figure: H; F; H′; G; H′′]

[figure: H; d_{0}; F; H′; d′_{0}; G; H′′; d′′_{0}]

[figure: H; d_{1}; F; H′; d′_{1}; G; H′′; d′′_{1}]

To see that ‘composition’ is preserved for the composite we must establish the commutativity of

H ×_{H} H \overline{\begin{matrix}⟨GF fst, GF snd⟩ & H_{′′} \\  \end{matrix}}H′′ ×_{H′′} H′′

[figure: H; comp; GF; H′′; comp′′]

given the commutativity of

[figure: H ×_{H} H; ⟨F fst, F snd⟩_{H′}; H′ ×_{H′} H′; ⟨Gfst′, Gsnd′⟩_{H′′}; H′′ ×_{H′′} H′′]

[figure: H; comp; F; H′; comp′; G; H′′; comp′′]

so it suffices to show that ⟨Gfst′, Gsnd′⟩_{H′′}⟨F fst, F snd⟩_{H′} = ⟨GF fst, GF snd⟩_{H′′}. But observe that we have

fst′′⟨Gfst′, Gsnd′⟩_{H′′}⟨F fst, F snd⟩_{H′} = Gfst′⟨F fst, F snd⟩_{H′} = GF fst

and

snd′′⟨Gfst′, Gsnd′⟩_{H′′}⟨F fst, F snd⟩_{H′} = Gsnd′⟨F fst, F snd⟩_{H′} = GF snd

so that ⟨Gfst′, Gsnd′⟩_{H′′}⟨F fst, F snd⟩_{H′} has the property which uniquely characterizes ⟨GF fst, GF snd⟩_{H′′}, namely that it fits into the pullback diagram

H ×_{H} H

[figure: H′′ ×_{H′′} H′′; snd′′; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; H′′; GF snd]

[figure: H′′; fst′′; d′′_{1}; GF fst; H′′; d′′_{0}]

• Identities exist: The identity internal functor for an internal category (H, d_{0}, d_{1}, comp) is just the identity arrow on H. We need to check that id_{H} is an internal functor; preservation of ‘domain’ and ‘codomain’ is trivial, and preservation of ‘composition’ again follows from the universal property of the pullback. That is, we have that ⟨id_{H}fst, id_{H}snd⟩_{H} = id_{H×_{H}H}, so that (F2) commutes for H′ = H and F = id_{H}. That these identites behave correctly under composition follows directly from the behavior of identity arrows in C.

• Composition is associative: Associativity of composition in Int(C) is again a direct conseqence of associativity of composition in C.

▷ Proposition: Let C be a finitely complete U-small category. Then Int(C) is finitely complete. Proof:

• Terminal object: The terminal object of Int(C) is the internal category whose ‘object of homomorphisms’ H is the terminal object 1_{C} of C. The arrows d_{0}, d_{1}, comp are all then necessarily the unique endomorphism !: 1_{C} → 1_{C}. The universal property of the terminal object of Int(C) is satisfied precisely because it is satisfied for the terminal object of C.

• Pairwise products: Suppose (H, d_{0}, d_{1}, comp), (H′, d′_{0}, d′_{1}, comp′) are two internal categories in C. We define the product in Int(C) ‘pointwise’, i.e. (H × H′, d_{0} × d′_{0}, d_{1} × d′_{1}, comp × comp′). There appears to be a type mismatch; the type of comp×comp′ is (H ×_{H} H)×(H′×_{H′} H′) → H ×H′, and we want it to be (H ×H′)×_{H×H′} (H ×H′) → H ×H′. However, (H × H′) ×_{H×H′} (H × H′) and (H ×_{H} H) × (H′ ×_{H′} H′) are uniquely isomorphic since × is a right adjoint and so preserves limits, in particular pullback diagrams. That H × H′ et al. is in fact an internal category follows from further application of preservation of limits by the product. It remains to check that the universal property of the product holds; suppose we have an internal category (H′′, d′′_{0}, d′′_{1}, comp′′) and internal functors F: H′′ → H and G: H′′ → H′. Now ⟨F, G⟩ (where pairing is in C) is the unique morphism in C such that L⟨F, G⟩ = F and R⟨F, G⟩ = G, where L, R are the projections from H × H′, again in C. It is easy to check that these projections are in fact internal functors, and that the pairing is an internal functor.

• Equalizers: Suppose we have two internal parallel functors

H  [figure: F; G] H′

we can find the equalizer in C to obtain an object H′′ and an arrow E: H′′ → H in C:

[figure: H′′; E; H; F; G; H′]

Our first priority is to find structure to make H′′ an internal category. Consider the diagram

[figure: H′′; E; H; F; G; H′; H′′; E; H; d_{0}; F; G; H′; d′_{0}]

and notice that since F, G are internal functors and E equalizes F, G, we have F d_{0}E = d′_{0}F E = d′_{0}GE = Gd_{0}E. That is, d_{0}E also equalizes F, G, which provides us an arrow d′′_{0}: H′′ → H′′ such that the following diagram commutes:

[figure: H′′; E; H; F; G; H′; H′′; d′′_{0}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; E; H; d_{0}; F; G; H′; d′_{0}]

Similarly, we get d′′_{1} out of the diagram

[figure: H′′; E; H; F; G; H′; H′′; d′′_{1}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; E; H; d_{1}; F; G; H′; d′_{1}]

since d_{1}E equalizes F, G, and we get comp′′ out of the diagram

[figure: H′′; E; H; F; G; H′]

H′′ ×_{H′′} H′′ comp′′ . . . . . . . . . . . . . . . . . ⟨Efst′′, Esnd′′⟩_{H} H ×_{H} H comp \frac{⟨F fst, F snd⟩_{H′}}{} ⟨Gfst, Gsnd⟩_{H′} H′ ×_{H′} H′ comp′

and observing that

⟨F fst, F snd⟩_{H′}⟨Efst′′, Esnd′′⟩_{H} = ⟨F Efst′′, F Esnd′′⟩_{H}
= ⟨GEfst′′, GEsnd′′⟩_{H}
= ⟨Gfst, Gsnd⟩_{H′}⟨Efst′′, Esnd′′⟩_{H}

Now it is easy to check that (H′′, d′′_{0}, d′′_{1}, comp′′) is an internal category; for example, by choice d′′_{0} is the unique arrow such that Ed′′_{0} = d_{0}E, yet Ed′′_{1}d′′_{0} = d_{1}Ed′′_{0} = d_{1}d_{0}E = d_{0}E, so it must be that d′′_{1}d′′_{0} = d′′_{0}. It falls out of the diagrams already shown that E is an internal functor H′′ → H. Now suppose we have a situation as depicted in the diagram

[figure: H′′; E; H; F; G; H′; H^{(3)}; I; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; J]

where H^{(3)} is an internal category and I is an internal functor equalizing F, G. The universal property of the equalizer in C guarantees a unique arrow J making the diagram commute. To see that J is internal functorial, consider the following diagram:

H′′  \overline{d′′_{0}} H′′

[figure: H; d_{0}; E; H; E]

[figure: H^{(3)}; J; d_{0}^{(3)}; I; H^{(3)}; J; I]

the internal trapezoids commute because E, I are internal functors, and the triangles commute by choice of J. Hence Ed′′_{0}J = EJd_{0}^{(3)}, and because E (being an equalizer) is mono, we know d′′_{0}J = Jd_{0}^{(3)}. The proofs that J preserves ‘codomain’ and ‘composition’ are similar. Therefore we conclude that E is the equalizer of F, G in Int(C).

▷ Proposition: C ↦ Int(C) as defined above is the object part of a functor Int: Fcc → Fcc. Proof: Let F: C → D be an arrow in Fcc, i.e. a finite limit preserving functor from C to D. Now Int(F) also needs to be a finite limit preserving functor, but from Int(C) to Int(D). Suppose we have an internal category (H, d_{0}, d_{1}, comp) in C. Then we define Int(F)(H, d_{0}, d_{1}, comp) := (FH, Fd_{0}, Fd_{1}, Fcomp). Because F preserves composition and finite products, (FH, Fd_{0}, Fd_{1}, Fcomp) is an internal category in D. The action of Int(F) on arrows of Int(C) is the obvious one; Int(F)(F) := FF. Now it is possible to see that Int(F) is functorial since Int(F)(id_{H}) = F(id_{H}) = id_{FH} = id_{Int(F)(H)} for any internal category object H in C, and Int(F)(G ∘ F) = F(G ∘ F) = F(G) ∘ F(F) = Int(F)(G) ∘ Int(F)(F) for any internal functors F: H → H′ and G: H′ → H′′ in C. Now we check that Int(F) preserves finite limits; We have first of all that Int(F)(1_{Int(C)}) = (F1_{Int(C)}, F!, F!, F!) = (1_{Int(D)},!,!,!) because F preserves the terminal object. Moreover, just by unrolling definitions again we see

Int(F)((H, d_{0}, d_{1}, comp) × (H′, d′_{0}, d′_{1}, comp′)) = Int(F)(H × H′, d_{0} × d′_{0}, d_{1} × d′_{1}, comp × comp′)
= (F(H × H′), F(d_{0} × d′_{0}), F(d_{1} × d′_{1}), F(comp × comp′))
= (FH × FH′, Fd_{0} × Fd′_{0}, Fd_{1} × Fd′_{1}, Fcomp × Fcomp′)
= (FH, Fd_{0}, Fd_{1}, Fcomp) × (FH′, Fd′_{0}, Fd′_{1}, Fcomp′)
= (FH, Fd_{0}, Fd_{1}, Fcomp) × (FH′, Fd′_{0}, Fd′_{1}, Fcomp′)
= Int(F)(H, d_{0}, d_{1}, comp) × Int(F)(H′, d′_{0}, d′_{1}, comp′)

and similarly Int(F) preserves equalizers because F does. Finally, we want Int itself to be functorial. Suppose we have arrows F: C → D and G: D → E in Fcc. Then

Int(G ∘ F)(H, d_{0}, d_{1}, comp) = ((G ∘ F)(H), (G ∘ F)(d_{0}), (G ∘ F)(d_{1}), (G ∘ F)(comp))
= (G(F(H)), G(F(d_{0})), G(F(d_{1})), G(F(comp)))
= Int(G)(F(H), F(d_{0}), F(d_{1}), F(comp))
= Int(G)(Int(F)(H, d_{0}, d_{1}, comp))
= (Int(G) ∘ Int(F))(H, d_{0}, d_{1}, comp)

and for any object C of Fcc we know

Int(id_{C})(H, d_{0}, d_{1}, comp) = (id_{C}(H), id_{C}(d_{0}), id_{C}(d_{1}), id_{C}(comp))
= (H, d_{0}, d_{1}, comp)

and so Int(id_{C}) = id_{Int(C)}, hence Int: Fcc → Fcc is functorial. ▷ Conjecture: There exists a functor Ext: Fcc → Fcc such that Int ⊣ Ext. ▷ Conjecture: Fcc is countably cocomplete. ▷ Corollary: There exists a finitely complete U-small category C such that Int(C) ≅ C.

Proof: Let Sets_{V} be the (U-small) category of all V-small sets. There exists a functor F: Sets_{V} → Int(Sets_{V}) defined by

F (S) := (S, id_{S}, id_{S}, id_{S})

and

F (f) := f

So we can form the diagram

[figure: D; :=; Sets_{V}; f; Int(Sets_{V}); Int(f); Int^{2}(Sets_{V}); Int^{2}(f); ⋯]

and set C := lim_{⟶} D to obtain

[figure: Sets_{V}; f; Int(Sets_{V}); Int(f); Int^{2}(Sets_{V}); Int^{2}(f); ⋯]

⋯

[figure: C; i_{1}; i_{2}; i_{0}]

Now Int, being a left adjoint, preserves colimits, so we have that

[figure: Int(Sets_{V}); Int(f); Int^{2}(Sets_{V}); Int^{2}(f); Int^{3}(Sets_{V}); Int^{3}(f); ⋯]

⋯

[figure: Int(C); Int(i_{1}); Int(i_{2}); Int(i_{0})]

is also a colimit diagram. That is, Int(C) = lim_{⟶} Int(D). Now if we can show that C is the colimit of Int(D), then C ≅ Int(C). Certainly C together with i_{1}, i_{2}, i_{3}, … is a cocone over Int(D), so there exists a unique h: Int(C) → C such that

Int^{n+1}(Sets_{V})

[figure: Int(C); h; Int(i_{n}); C; i_{n+1}]

commutes for every n ∈ ℕ. Also Int(C) together with Int(i_{0}) ∘ f, Int(i_{0}), Int(i_{1}), Int(i_{2}), … is a cocone over D, so there exists a unique k: C → Int(C) such that

Sets_{V}

[figure: Int(C); k; Int(i_{0}) ∘ f; C; i_{0}]

commutes and

Int^{n+1}(Sets_{V})

[figure: Int(C); k; Int(i_{n}); C; i_{n+1}]

commutes for every n ∈ ℕ. Notice that h, k are morphisms in the category of cocones over Int(D), and therefore so too is k ∘ h: Int(C) → Int(C). Hence kh = id_{Int(C)} since Int(C) = lim_{⟶} Int(D). But h, k are also morphisms in the category of cocones over D (h is because h ∘ Int(i_{0}) ∘ f = i_{1} ∘ f = i_{0}) so hk = id_{C} since C = lim_{⟶} D. That is, h, k are an inverse pair, and C ≅ Int(C).