proposition: Lemma discrete_cat_property : forall z, subcategory_property (function_cat z) (fun x => True) is_id_fun_arrow.
proof: Proof. ir. uhg; ee. ap function_cat_axioms. ir. uhg; ee. rw source_comp. cp H2; cp H3. rwi is_id_fun_arrow_rw H2. rwi is_id_fun_arrow_rw H3. ee. cp H. rwi mor_function_cat3 H8. ee. cp (H7 z H9). rw H13. rw left_id. uh H5. am. rww ob_function_cat. am. sy; am. tv. am. am. am. ir. clear H0. cp H. rwi ob_function_cat H0. rww id_function_cat. uhg. rww source_fa_id. ir. tv. ir. tv. Qed.
imports: Arith ordinal nat_trans