proposition: Lemma functor_vee_eq2 : forall a u v f, Functor.axioms f -> source f = vee_cat -> a = target f -> u = (fmor f (catyd_arrow a12')) -> v = (fmor f (catyd_arrow a32')) -> f = vee_functor a u v.
proof: Proof. ir. rw H1; rw H2; rw H3; app functor_vee_eq. Qed.
imports: Arith cat_examples cardinal fc_limits