proposition: Lemma mor_twoarrow_cat : forall (y:morsy twoarrow_data), mor twoarrow_cat (catyd_arrow y).
proof: Proof. ir. uf twoarrow_cat. app mor_catyd_catyd_arrow. ap twoarrow_data_property. Qed.
imports: Arith cat_examples cardinal fc_limits