proposition: Lemma mor_discrete_cat : forall z u, mor (discrete_cat z) u = (inc (source u) z & is_id_fun_arrow u).
proof: Proof. ir. uf discrete_cat. rw mor_subcategory. ap iff_eq; ir. xd. rwi mor_function_cat3 H. ee; am. xd. uh H0; ee. assert (u = id (function_cat z) (source u)). rw id_function_cat. am. am. rw H1. ap mor_id. rww ob_function_cat. ap discrete_cat_property. Qed.
imports: Arith ordinal nat_trans