proposition: Lemma htrans_right_vee_functor : forall y a u v, Nat_Trans.axioms y -> vee_hypothesis a u v -> osource y = a -> htrans_right y (vee_functor a u v) = vee_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)) (ntrans y (source v)).
proof: Proof. ir. wr H1. wri H1 H0. cp vee_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 vee_functor_axioms. am. rww target_vee_functor. ap vee_nt_axioms. app vee_nt_hypothesis_for_htrans_right. rw source_htrans_right. rw fcompose_vee_functor. rw source_vee_nt. rww target_source. am. am. tv. rw target_htrans_right. rw fcompose_vee_functor. rw target_vee_nt. reflexivity. am. am. rww source_target. ir. rwi osource_htrans_right H12. cp H12. rwi source_vee_functor H13. rww ntrans_htrans_right. rwi ob_vee_cat_ex H13. nin H13. nin x0; rw H13. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. rw fob_vee_functor_R. rw ntrans_vee_nt_R. reflexivity. am. Qed.
imports: Arith cat_examples cardinal fc_limits