proposition: Lemma vcompose_twoarrow_nt : forall a u1 v1 u2 v2 r s u1' v1' u2' v2' r' s', twoarrow_nt_hypothesis a u1 v1 u2 v2 r s -> twoarrow_nt_hypothesis a u1' v1' u2' v2' r' s' -> u1 = u2' -> v1 = v2' -> vcompose (twoarrow_nt a u1 v1 u2 v2 r s) (twoarrow_nt a u1' v1' u2' v2' r' s') = twoarrow_nt a u1' v1' u2 v2 (comp a r r') (comp a s s').
proof: Proof. ir. wr H1. wr H2. wri H1 H0; wri H2 H0. cp twoarrow_cat_axioms. cp H; cp H0. uh H4; uh H5. ee. assert (twoarrow_hypothesis a u1 v1). uhg; ee; am. assert (twoarrow_hypothesis a u2 v2). uhg; ee; am. assert (twoarrow_hypothesis a u1' v1'). uhg; ee; am. cp (twoarrow_functor_axioms H38). cp (twoarrow_functor_axioms H39). cp (twoarrow_functor_axioms H40). assert (ob a (source u1)). rww ob_source. assert (ob a (target u1)). rww ob_target. assert (ob a (source u2)). rww ob_source. assert (ob a (target u2)). rww ob_target. assert (ob a (source u1')). rww ob_source. assert (ob a (target u1')). rww ob_target. cp (twoarrow_nt_axioms H). cp (twoarrow_nt_axioms H0). assert (source r = target r'). rww H13. assert (source s = target s'). rww H15. assert (twoarrow_nt_hypothesis a u1' v1' u2 v2 (comp a r r') (comp a s s')). uhg; ee. uh H6; ee; am. am. am. am. am. rww mor_comp. rww mor_comp. rww source_comp. rww target_comp. rww source_comp. rww target_comp. am. am. am. am. rww assoc. rw H20. wrr assoc. rw H36. rww assoc. sy; am. sy; am. rww assoc. rw H21. wrr assoc. rw H37. rww assoc. wr H34. sy; am. wr H33. am. wr H32. sy; am. wr H17; am. ap Nat_Trans.axioms_extensionality. rw vcompose_axioms. tv. am. am. rw source_twoarrow_nt. rw target_twoarrow_nt. reflexivity. app twoarrow_nt_axioms. rw source_vcompose. rw source_twoarrow_nt. rw source_twoarrow_nt. reflexivity. rw target_vcompose. rw target_twoarrow_nt. rw target_twoarrow_nt. reflexivity. ir. rwi osource_vcompose H55. rwi osource_twoarrow_nt H55. rw ntrans_vcompose. rw otarget_twoarrow_nt. rwi ob_twoarrow_cat_or H55. nin H55. rw H55. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. reflexivity. rw H55. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. reflexivity. rw osource_twoarrow_nt. am. Qed.
imports: Arith cat_examples cardinal fc_limits