proposition: Lemma htrans_left_twoarrow_nt : forall a u1 v1 u2 v2 r s f, twoarrow_nt_hypothesis a u1 v1 u2 v2 r s -> Functor.axioms f -> source f = a -> htrans_left f (twoarrow_nt a u1 v1 u2 v2 r s) = twoarrow_nt (target f) (fmor f u1) (fmor f v1) (fmor f u2) (fmor f v2) (fmor f r) (fmor f s).
proof: Proof. ir. wr H1. wri H1 H. cp twoarrow_cat_axioms. cp H. uh H3. ee. assert (twoarrow_hypothesis (source f) u1 v1). uhg; ee; am. assert (twoarrow_hypothesis (source f) u2 v2). uhg; ee; am. cp (twoarrow_functor_axioms H20). cp (twoarrow_functor_axioms H21). assert (ob (source f) (source u1)). rww ob_source. assert (ob (source f) (source u2)). rww ob_source. assert (ob (source f) (target u1)). rww ob_target. assert (ob (source f) (target u2)). rww ob_target. cp (twoarrow_nt_axioms H). ap Nat_Trans.axioms_extensionality. app htrans_left_axioms. rww otarget_twoarrow_nt. app twoarrow_nt_axioms. app twoarrow_nt_hypothesis_for_htrans_left. rww source_htrans_left. rww source_twoarrow_nt. rw source_twoarrow_nt. rw fcompose_twoarrow_functor. tv. am. am. tv. rw target_htrans_left. rw target_twoarrow_nt. rw fcompose_twoarrow_functor. rw target_twoarrow_nt. tv. am. am. tv. ir. rwi osource_htrans_left H29. rwi osource_twoarrow_nt H29. rw ntrans_htrans_left. rwi ob_twoarrow_cat_or H29. nin H29. rw H29. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. reflexivity. rw H29. rw ntrans_twoarrow_nt_R. rw ntrans_twoarrow_nt_R. reflexivity. rww osource_twoarrow_nt. Qed.
imports: Arith cat_examples cardinal fc_limits