I've been thinking about pushouts in category theory recently, and found a quick theorem about categories with pushouts that I haven't seen anywhere. Cartesian closure of pushouts Theorem: Let C be a category, and D a category with pushouts. Then the functor category C → D also has pushouts. Proof: Let us consider the construction of an arbitrary pushout in C → D. We have three functors F, G, H : C → D, and two natural transformations α : F → G and β : F → H. We must define a new ...
