proposition: Lemma has_limits_functor_cat : forall a b z, Category.axioms a -> Category.axioms b -> Category.axioms z -> has_limits_over z b -> has_limits_over z (functor_cat a b).
proof: Proof. ir. uhg; ee. ir. apply presheaf_limit_criterion with a b. am. am. am. am. ir. uh H2; ee. ap H2. app pointf_axioms. rww source_pointf. rww target_pointf. Qed.
imports: Arith colimits functor_cat