proposition: Lemma vee_nt_hypothesis_for_htrans_right : forall y u v, Nat_Trans.axioms y -> vee_hypothesis (osource y) u v -> vee_nt_hypothesis (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. cp vee_cat_axioms. cp H0. uh H2; ee. assert (ob (osource y) (source u)). rww ob_source. assert (ob (osource y) (target u)). rww ob_target. assert (ob (osource y) (source v)). rww ob_source. 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. uhg; ee. am. wrr target_source; app mor_fmor. wrr target_source; app mor_fmor. wrr target_target; app mor_fmor; rww source_target. wrr target_target; app mor_fmor; rww source_target. app mor_ntrans. app mor_ntrans. app mor_ntrans. rww source_ntrans. rww source_fmor. rww target_ntrans. rww source_fmor. rww source_target. rww source_ntrans. rww target_fmor. rww target_ntrans. rww target_fmor. rww source_target. rww source_ntrans. rww source_fmor. rww target_ntrans. rww source_fmor. rww source_target. rww target_fmor. rww target_fmor. rww H4. rww target_fmor. rww target_fmor. rww H4. rww source_target. rww source_target. rww carre. rw H4. rww carre. Qed.
imports: Arith cat_examples cardinal fc_limits