proposition: Lemma nttyd_axioms : forall d f g (n:obsy d -> E), nttyd_property f g n -> Nat_Trans.axioms (nttyd f g n).
proof: Proof. ir. assert (lem1: catyd_property d). uh H; ee. uh H0; ee; am. assert (lem2: Category.axioms (catyd d)). app catyd_axioms. assert (lem3 : funtyd_property f). uh H; ee; am. assert (lem4 : funtyd_property g). uh H; ee; am. assert (lem5 : Functor.axioms (funtyd f)). app funtyd_axioms. assert (lem6 : Functor.axioms (funtyd g)). app funtyd_axioms. uhg; ee. uf nttyd. ap create_like. rww osource_nttyd. rw otarget_nttyd. uh H; ee. uh H1; ee. am. rww source_nttyd. rww target_nttyd. rww target_nttyd. rww osource_nttyd. rww source_funtyd. rww source_nttyd. rww otarget_nttyd. rww target_funtyd. uh H; ee; am. ir. rw otarget_nttyd. rwi osource_nttyd H0. cp H0. rw ntrans_nttyd. rwi ob_catyd H1. nin H1. rw H1. rw X_rewrite. uh H; ee. wr H4; au. am. am. ir. rwi osource_nttyd H0. cp H0. rwi ob_catyd H0. nin H0. rww ntrans_nttyd. rww source_nttyd. rw H0. rw X_rewrite. rw fob_funtyd_R. uh H; ee. ap H6. am. am. ir. rwi osource_nttyd H0. cp H0. rwi ob_catyd H0. nin H0. rw H0. rw ntrans_nttyd_R. rw target_nttyd. rw fob_funtyd_R. uh H; ee; au. am. am. am. ir. rwi osource_nttyd H0. cp H0. rwi mor_catyd H1. nin H1. rw H1. rw target_catyd_arrow. rw ntrans_nttyd_R. rw otarget_nttyd. rw source_nttyd. rw fmor_funtyd_catyd_arrow. rw target_nttyd. rw fmor_funtyd_catyd_arrow. rw source_catyd_arrow. rw ntrans_nttyd_R. uh H; ee. wr H4. ap H8. am. am. am. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits