proposition: Lemma mor_catyd : forall d u, catyd_property d -> mor (catyd d) u = (exists v : morsy d, u = catyd_arrow v).
proof: Proof. ir. ap iff_eq; ir. uh H0; ee. ufi catyd H1. rwi Category.is_mor_create H1. rwi inc_catyd_arrow_set H1. am. uhg; ee. app catyd_axioms. uf catyd. rw Category.is_mor_create. rw inc_catyd_arrow_set. am. Qed.
imports: Arith cat_examples cardinal fc_limits