proposition: Lemma vee_nt_hypothesis_ntrans : forall u, Nat_Trans.axioms u -> osource u = vee_cat -> vee_nt_hypothesis (otarget u) (fmor (source u) (catyd_arrow a12')) (fmor (source u) (catyd_arrow a32')) (fmor (target u) (catyd_arrow a12')) (fmor (target u) (catyd_arrow a32')) (ntrans u (R o1')) (ntrans u (R o2')) (ntrans u (R o3')).
proof: Proof. ir. assert (Category.axioms (otarget u)). rww category_axioms_otarget. assert (Functor.axioms (source u)). rww functor_axioms_source. assert (Functor.axioms (target u)). rww functor_axioms_target. uhg; ee. am. wrr target_source. app mor_fmor. rw source_source. rw H0. ap mor_vee_cat. wr target_source. app mor_fmor. rw source_source. rw H0. ap mor_vee_cat. am. uf otarget. app mor_fmor. rw source_target. rw H0. ap mor_vee_cat. am. uf otarget. app mor_fmor. rw source_target. rw H0. ap mor_vee_cat. am. app mor_ntrans. rw H0. ap ob_vee_cat. app mor_ntrans. rw H0. ap ob_vee_cat. app mor_ntrans. rw H0. ap ob_vee_cat. rww source_fmor. rww source_catyd_arrow. rww source_ntrans. rw H0. ap ob_vee_cat. rw source_source; rw H0; ap mor_vee_cat. rww target_ntrans. rww source_fmor. rww source_catyd_arrow. rww source_target. rw H0. ap mor_vee_cat. rw H0. ap ob_vee_cat. rww source_ntrans. rww target_fmor. rww target_catyd_arrow. rw source_source; rw H0; ap mor_vee_cat. rw H0. ap ob_vee_cat. rww target_ntrans. rww target_fmor. rww target_catyd_arrow. rww source_target. rw H0. ap mor_vee_cat. rw H0. ap ob_vee_cat. rww source_ntrans. rww source_fmor. rww source_catyd_arrow. rw source_source. rw H0. ap mor_vee_cat. rw H0. ap ob_vee_cat. rww target_ntrans. rww source_fmor. rww source_catyd_arrow. rw source_target. rw H0. ap mor_vee_cat. am. rw H0. ap ob_vee_cat. rw target_fmor. rw target_catyd_arrow. rw target_fmor. rw target_catyd_arrow. reflexivity. am. rw source_source; rw H0; ap mor_vee_cat. am. rw source_source; rw H0; ap mor_vee_cat. rw target_fmor. rw target_catyd_arrow. rw target_fmor. rw target_catyd_arrow. reflexivity. am. rww source_target; rw H0; ap mor_vee_cat. am. rww source_target; rw H0; ap mor_vee_cat. assert (R o2' = target (catyd_arrow a12')). rww target_catyd_arrow. rw H4. rw carre. rw source_catyd_arrow. reflexivity. am. rw H0. ap mor_vee_cat. assert (R o2' = target (catyd_arrow a32')). rww target_catyd_arrow. rw H4. rw carre. rw source_catyd_arrow. reflexivity. am. rw H0. ap mor_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits