proposition: Lemma htrans_right_twoarrow_functor : forall y a u v, Nat_Trans.axioms y -> twoarrow_hypothesis a u v -> osource y = a -> htrans_right y (twoarrow_functor a u v) = twoarrow_nt (otarget y) (fmor (source y) u) (fmor (source y) v) (fmor (target y) u) (fmor (target y) v) (ntrans y (source u)) (ntrans y (target u)).
proof: Proof. ir. wr H1. wri H1 H0. cp twoarrow_cat_axioms. cp H0. uh H3; ee. assert (ob (osource y) (source u)). rww ob_source. assert (ob (osource y) (target u)). rww ob_target. assert (Functor.axioms (source y)). rww functor_axioms_source. assert (Functor.axioms (target y)). rww functor_axioms_target. assert (Category.axioms (osource y)). rww category_axioms_osource. assert (Category.axioms (otarget y)). rww category_axioms_otarget. ap Nat_Trans.axioms_extensionality. ap htrans_right_axioms. app twoarrow_functor_axioms. am. rww target_twoarrow_functor. ap twoarrow_nt_axioms. app twoarrow_nt_hypothesis_for_htrans_right. rw source_htrans_right. rw fcompose_twoarrow_functor. rw source_twoarrow_nt. rww target_source. am. am. tv. rw target_htrans_right. rw fcompose_twoarrow_functor. rw target_twoarrow_nt. reflexivity. am. am. rww source_target. ir. rwi osource_htrans_right H13. cp H13. rwi source_twoarrow_functor H14. rww ntrans_htrans_right. rwi ob_twoarrow_cat_or H14. nin H14; rw H14. rw fob_twoarrow_functor_R. rw ntrans_twoarrow_nt_R. reflexivity. am. rw fob_twoarrow_functor_R. rw ntrans_twoarrow_nt_R. reflexivity. am. Qed.
imports: Arith cat_examples cardinal fc_limits