proposition: Lemma functor_twoarrow_eq : forall f, Functor.axioms f -> source f = twoarrow_cat -> f = twoarrow_functor (target f) (fmor f (catyd_arrow a0')) (fmor f (catyd_arrow a1')).
proof: Proof. ir. ap Functor.axioms_extensionality. am. ap twoarrow_functor_axioms. app functor_twoarrow_hypothesis. rww source_twoarrow_functor. rww target_twoarrow_functor. ir. rwi H0 H1. set (p:= (fmor f (catyd_arrow (d:=twoarrow_data) a0'))). set (q:= (fmor f (catyd_arrow (d:=twoarrow_data) a1'))). rwi mor_twoarrow_cat_ex H1. nin H1. rw H1. rw fmor_twoarrow_functor_catyd_arrow. assert (catyd_arrow (d:= twoarrow_data) i1 = id twoarrow_cat (R o1')). rw id_twoarrow_cat_R. reflexivity. assert (catyd_arrow (d:= twoarrow_data) i2 = id twoarrow_cat (R o2')). rw id_twoarrow_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_twoarrow_cat. am. tv. rw H0; ap ob_twoarrow_cat. rw H3. wr H0. rw fmor_id. uf p. rw target_fmor. rw target_catyd_arrow. reflexivity. am. rw H0; ap mor_twoarrow_cat. am. tv. rw H0; ap ob_twoarrow_cat. reflexivity. reflexivity. uf p. uf q. app functor_twoarrow_hypothesis. Qed.
imports: Arith cat_examples cardinal fc_limits