proposition: Lemma vee_functor_axioms : forall a u v, vee_hypothesis a u v -> Functor.axioms (vee_functor a u v).
proof: Proof. ir. uh H; ee. uf vee_functor. ap funtyd_axioms. app vee_fun_data_property. uhg; ee; am. Qed.
imports: Arith cat_examples cardinal fc_limits