proposition: Lemma fidentity_vee_cat : fidentity vee_cat = vee_functor vee_cat (catyd_arrow a12') (catyd_arrow a32').
proof: Proof. cp vee_cat_axioms. app functor_vee_eq2. rww fidentity_axioms. rww source_fidentity. rww target_fidentity. rww fmor_fidentity. ap mor_vee_cat. rww fmor_fidentity; ap mor_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits