proposition: Lemma mor_twoarrow_cat_ex : forall u, mor twoarrow_cat u = (exists y:morsy twoarrow_data, u = catyd_arrow y).
proof: Proof. ir. ap iff_eq; ir. ufi twoarrow_cat H; rwi mor_catyd H. am. ap twoarrow_data_property. nin H. rw H. ap mor_twoarrow_cat. Qed.
imports: Arith cat_examples cardinal fc_limits