proposition: Lemma twoarrow_nt_ntrans : forall u, Nat_Trans.axioms u -> osource u = twoarrow_cat -> twoarrow_nt (otarget u) (fmor (source u) (catyd_arrow a0')) (fmor (source u) (catyd_arrow a1')) (fmor (target u) (catyd_arrow a0')) (fmor (target u) (catyd_arrow a1')) (ntrans u (R o1')) (ntrans u (R o2')) = u.
proof: Proof. ir. ap Nat_Trans.axioms_extensionality. ap twoarrow_nt_axioms. app twoarrow_nt_hypothesis_ntrans. am. rw source_twoarrow_nt. wr target_source. sy; ap functor_twoarrow_eq. uh H; ee. am. am. am. rw target_twoarrow_nt. uf otarget. sy; ap functor_twoarrow_eq. uh H; ee; am. rww source_target. ir. ufi osource H1. rwi source_twoarrow_nt H1. rwi source_twoarrow_functor H1. rwi ob_twoarrow_cat_or H1. nin H1. rw H1. rw ntrans_twoarrow_nt_R. reflexivity. rw H1. rw ntrans_twoarrow_nt_R. reflexivity. Qed.
imports: Arith cat_examples cardinal fc_limits