proposition: Lemma has_coequalizers_functor_cat : forall a b, Category.axioms a -> has_coequalizers b -> has_coequalizers (functor_cat a b).
proof: Proof. ir. rw has_coequalizers_has_colimits_over_opp. cp H0. uh H1; ee. rwi has_coequalizers_has_colimits_over_opp H0. ap has_colimits_functor_cat. am. am. ap opp_axioms. ap twoarrow_cat_axioms. am. am. ap functor_cat_axioms. am. uh H0; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal