proposition: Lemma functor_vee_hypothesis : forall f, Functor.axioms f -> source f = vee_cat -> vee_hypothesis (target f) (fmor f (catyd_arrow a12')) (fmor f (catyd_arrow a32')).
proof: Proof. ir. uhg; ee. app mor_fmor. rw H0. ap mor_vee_cat. app mor_fmor. rw H0. ap mor_vee_cat. rww target_fmor. rw target_catyd_arrow. rww target_fmor. rww target_catyd_arrow. rw H0. ap mor_vee_cat. rw H0. ap mor_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits