proposition: Lemma functor_vee_eq : forall f, Functor.axioms f -> source f = vee_cat -> f = vee_functor (target f) (fmor f (catyd_arrow a12')) (fmor f (catyd_arrow a32')).
proof: Proof. ir. ap Functor.axioms_extensionality. am. ap vee_functor_axioms. app functor_vee_hypothesis. rww source_vee_functor. rww target_vee_functor. ir. rwi H0 H1. set (p:= (fmor f (catyd_arrow (d:=vee_data) a12'))). set (q:= (fmor f (catyd_arrow (d:=vee_data) a32'))). rwi mor_vee_cat_ex H1. nin H1. rw H1. rw fmor_vee_functor_catyd_arrow. assert (catyd_arrow (d:= vee_data) i1 = id vee_cat (R o1')). rw id_vee_cat_R. reflexivity. assert (catyd_arrow (d:= vee_data) i2 = id vee_cat (R o2')). rw id_vee_cat_R. reflexivity. assert (lem1: catyd_arrow (d:= vee_data) i3 = id vee_cat (R o3')). rw id_vee_cat_R. reflexivity. nin x. rw H2. wr H0. rw fmor_id. uf p. rw source_fmor. rw source_catyd_arrow. tv. am. rw H0. ap mor_vee_cat. am. tv. rw H0; ap ob_vee_cat. rw H3. wr H0. rw fmor_id. uf p. rw target_fmor. rw target_catyd_arrow. reflexivity. am. rw H0; ap mor_vee_cat. am. tv. rw H0; ap ob_vee_cat. rw lem1. wr H0. rw fmor_id. uf q. rw source_fmor. rw source_catyd_arrow. reflexivity. am. rw H0; ap mor_vee_cat. am. tv. rw H0; ap ob_vee_cat. reflexivity. reflexivity. uf p. uf q. app functor_vee_hypothesis. Qed.
imports: Arith cat_examples cardinal fc_limits