proposition: Lemma htrans_left_vee_nt : forall a u1 v1 u2 v2 r s t f, vee_nt_hypothesis a u1 v1 u2 v2 r s t -> Functor.axioms f -> source f = a -> htrans_left f (vee_nt a u1 v1 u2 v2 r s t) = vee_nt (target f) (fmor f u1) (fmor f v1) (fmor f u2) (fmor f v2) (fmor f r) (fmor f s) (fmor f t).
proof: Proof. ir. wr H1. wri H1 H. cp vee_cat_axioms. cp H. uh H3. ee. assert (vee_hypothesis (source f) u1 v1). uhg; ee; am. assert (vee_hypothesis (source f) u2 v2). uhg; ee; am. cp (vee_functor_axioms H21). cp (vee_functor_axioms H22). 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. assert (ob (source f) (source v1)). rww ob_source. assert (ob (source f) (source v2)). rww ob_source. cp (vee_nt_axioms H). ap Nat_Trans.axioms_extensionality. app htrans_left_axioms. rww otarget_vee_nt. app vee_nt_axioms. app vee_nt_hypothesis_for_htrans_left. rww source_htrans_left. rww source_vee_nt. rw source_vee_nt. rw fcompose_vee_functor. tv. am. am. tv. rw target_htrans_left. rw target_vee_nt. rw fcompose_vee_functor. rw target_vee_nt. tv. am. am. tv. ir. rwi osource_htrans_left H32. rwi osource_vee_nt H32. rw ntrans_htrans_left. rwi ob_vee_cat_ex H32. nin H32. nin x0. rw H32. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rw H32. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rw H32. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rww osource_vee_nt. Qed.
imports: Arith cat_examples cardinal fc_limits