proposition: Lemma inclusion_cat_property : forall z, subcategory_property (function_cat z) (fun x => True) is_fa_inclusion.
proof: Proof. ir. uhg; ee. ap function_cat_axioms. ir. rw comp_function_cat. ap is_fa_inclusion_fa_comp. am. am. am. am. am. am. ir. rw id_function_cat. ap is_fa_inclusion_fa_id. rwi ob_function_cat H; am. ir; tv. ir; tv. Qed.
imports: Arith ordinal nat_trans