proposition: Lemma has_equalizers_has_limits_over : forall a, Category.axioms a -> has_equalizers a = has_limits_over twoarrow_cat a.
proof: Proof. ir. ap iff_eq; ir. uhg. ir. uh H0. ee. util (H4 (fmor f (catyd_arrow a0')) (fmor f (catyd_arrow a1'))). wr H3. ap functor_twoarrow_hypothesis. am. am. uh H5. ee. wri H3 H6. rww functor_twoarrow_eq. uh H0. uhg; ee. am. ir. uhg; ee; try am. ap H0. app twoarrow_functor_axioms. rww source_twoarrow_functor. rww target_twoarrow_functor. Qed.
imports: Arith colimits little_cat fc_limits cardinal