proposition: Lemma mor_function_cat1 : forall z u, mor (function_cat z) u = (Arrow.like u & inc (source u) z & inc (target u) z & inc u (function_arrow_set (source u) (target u))).
proof: Proof. ir. ap iff_eq. ir. ufi function_cat H. rwi mor_from_arrows H. ee. rwi inc_function_arrow_set H1. ee; am. rwi ob_from_arrows H. am. ap function_cat_property. rwi ob_from_arrows H0. am. ap function_cat_property. am. ap function_cat_property. ir. ee. uf function_cat. rw mor_from_arrows. ee. rw ob_from_arrows. am. ap function_cat_property. rw ob_from_arrows. am. ap function_cat_property. am. ap function_cat_property. Qed.
imports: Arith ordinal nat_trans