proposition: Lemma vee_nt_hypothesis_for_htrans_left : forall u1 v1 u2 v2 r s t f, vee_nt_hypothesis (source f) u1 v1 u2 v2 r s t -> Functor.axioms f -> vee_nt_hypothesis (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. cp vee_cat_axioms. cp H. uh H2. 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 H20). cp (vee_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. assert (ob (source f) (source v1)). rww ob_source. assert (ob (source f) (source v2)). rww ob_source. cp (vee_nt_axioms H). uhg; ee; try (app mor_fmor); try (rww source_fmor); try (rww source_fmor); try (rww target_fmor); try (rww target_fmor); try (app uneq). uh H0; ee; am. rww comp_fmor. rww comp_fmor. app uneq. sy; am. rww comp_fmor. rww comp_fmor. app uneq. sy; am. wrr H16. Qed.
imports: Arith cat_examples cardinal fc_limits