proposition: Lemma functor_cat_axioms : forall a b, Category.axioms a -> Category.axioms b -> Category.axioms (functor_cat a b).
proof: Proof. ir. uf functor_cat. ap Category.create_axioms. uhg; ee; ir. rw inc_functor_set; app iff_eq; ir. uh H1; ee. uhg; ee. rw inc_functor_set. uhg; xd. rw inc_nt2_set. uhg; ee. rww vident_axioms. rww osource_vident. rww otarget_vident. rww source_vident. rww target_vident. uh H1; ee. rwi inc_functor_set H1. am. app iff_eq; ir. cp H1. rwi inc_nt2_set H2. uh H2; ee. uhg; ee. am. rw inc_functor_set. uhg; ee. uh H2; ee. am. am. rww target_source. rw inc_functor_set. uhg; ee. uh H2; ee; am. rww source_target. am. rww right_vident. rww left_vident. uh H2; ee. uh H2. ufi create H2. wr H2. rww Arrow.create_like. uh H1; ee. am. cp H1; cp H2. rwi inc_nt2_set H4. rwi inc_nt2_set H5. uh H4; uh H5; ee. uhg; ee. am. am. am. rw inc_nt2_set. uhg; ee. rww vcompose_axioms. rww osource_vcompose. rww otarget_vcompose. rww source_vcompose. rww target_vcompose. rww vcompose_assoc. rwi inc_nt2_set H1. lu. rwi inc_nt2_set H2. lu. rwi inc_nt2_set H3. lu. Qed.
imports: Arith nat_trans