proposition: Lemma mor_inclusion_cat : forall z u, mor (inclusion_cat z) u = (inc (source u) z & inc (target u) z & is_fa_inclusion u).
proof: Proof. ir. uf inclusion_cat. rw mor_subcategory. ap iff_eq; ir; xd. wr ob_function_cat. rww ob_source. wr ob_function_cat. rww ob_target. uh H1; ee. rw H2. rw mor_function_cat1. ee. uf fa_inclusion. rww Arrow.create_like. rw source_fa_inclusion. am. rww target_fa_inclusion. rw source_fa_inclusion. rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. ap inclusion_cat_property. Qed.
imports: Arith ordinal nat_trans