proposition: Lemma catyd_axioms : forall d, catyd_property d -> Category.axioms (catyd d).
proof: Proof. ir. uf catyd. ap Category.create_axioms. uhg; ee. ir. ap iff_eq; ir. uhg. ee. am. nin H0. wr H0. rw catyd_id_R. ap inc_catyd_arrow. nin H0. wr H0. rw catyd_id_R. rww source_catyd_arrow. uh H; ee. rw H. tv. nin H0. wr H0. rw catyd_id_R. rww target_catyd_arrow. uh H; ee. rw H1. tv. uh H0; ee. am. ir. ap iff_eq; ir. rwi inc_catyd_arrow_set H0. nin H0. rw H0. uhg; ee; try (rw source_catyd_arrow); try (rw target_catyd_arrow). rw inc_catyd_arrow_set. sh x. tv. ap R_inc. ap R_inc. rw catyd_id_R. rw catyd_comp_catyd_arrow. uh H; ee. rw H5. tv. rw catyd_id_R. rw catyd_comp_catyd_arrow. uh H; ee. rw H4. tv. uf catyd_arrow. rww Arrow.create_like. uh H0; ee; am. ir. rwi inc_catyd_arrow_set H0. rwi inc_catyd_arrow_set H1. nin H0; nin H1. rw H0; rw H1. uhg; ee. ap inc_catyd_arrow. ap inc_catyd_arrow. rw source_catyd_arrow. rw target_catyd_arrow. rwi H0 H2; rwi H1 H2. rwi source_catyd_arrow H2; rwi target_catyd_arrow H2. am. rw catyd_comp_catyd_arrow. ap inc_catyd_arrow. rw catyd_comp_catyd_arrow. rw source_catyd_arrow. rw source_catyd_arrow. uh H; ee. util (H4 x x0). ap R_inj. rwi H0 H2; rwi H1 H2. rwi source_catyd_arrow H2; rwi target_catyd_arrow H2. am. rww H9. uh H; ee. util (H5 x x0). ap R_inj. rwi H0 H2; rwi H1 H2. rwi source_catyd_arrow H2; rwi target_catyd_arrow H2. am. rw catyd_comp_catyd_arrow. rw target_catyd_arrow. rw target_catyd_arrow. rww H9. ir. rwi inc_catyd_arrow_set H0. rwi inc_catyd_arrow_set H1. rwi inc_catyd_arrow_set H2. nin H0; nin H1; nin H2. rwi H0 H3. rwi H1 H3. rwi H1 H4. rwi H2 H4. rwi source_catyd_arrow H3. rwi source_catyd_arrow H4. rwi target_catyd_arrow H3. rwi target_catyd_arrow H4. cp (R_inj H3). cp (R_inj H4). rw H0; rw H1; rw H2. rw catyd_comp_catyd_arrow. rw catyd_comp_catyd_arrow. rw catyd_comp_catyd_arrow. rw catyd_comp_catyd_arrow. uh H; ee. rw H12. reflexivity. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits