proposition: Lemma functor_twoarrow_hypothesis : forall f, Functor.axioms f -> source f = twoarrow_cat -> twoarrow_hypothesis (target f) (fmor f (catyd_arrow a0')) (fmor f (catyd_arrow a1')).
proof: Proof. ir. uhg; ee. app mor_fmor. rw H0. ap mor_twoarrow_cat. app mor_fmor. rw H0. ap mor_twoarrow_cat. rww source_fmor. rw source_catyd_arrow. rww source_fmor. rww source_catyd_arrow. rw H0. ap mor_twoarrow_cat. rw H0. ap mor_twoarrow_cat. rww target_fmor. rw target_catyd_arrow. rww target_fmor. rww target_catyd_arrow. rw H0. ap mor_twoarrow_cat. rw H0. ap mor_twoarrow_cat. Qed.
imports: Arith cat_examples cardinal fc_limits