proposition: Lemma has_fiprods_has_limits_over : forall a, Category.axioms a -> has_fiprods a = has_limits_over vee_cat a.
proof: Proof. ir. ap iff_eq; ir. uhg. ir. uh H0. ee. util (H4 (fmor f (catyd_arrow a12')) (fmor f (catyd_arrow a32'))). wr H3. ap functor_vee_hypothesis. am. am. uh H5. ee. wri H3 H6. rww functor_vee_eq. uh H0. uhg; ee. am. ir. uhg; ee; try am. ap H0. app vee_functor_axioms. rww source_vee_functor. rww target_vee_functor. Qed.
imports: Arith colimits little_cat fc_limits cardinal