proposition: Lemma has_finite_colimits_functor_cat : forall a b, Category.axioms a -> has_finite_colimits b -> has_finite_colimits (functor_cat a b).
proof: Proof. ir. uh H0; uhg; ee. app functor_cat_axioms. ir. ap has_colimits_functor_cat. am. am. uh H2; ee; am. app H1. Qed.
imports: Arith cat_examples cardinal fc_limits