proposition: Lemma mor_function_cat3 : 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)) & Map.axioms (source u) (target u) (arrow u)).
proof: Proof. ir. ap iff_eq; ir. cp H. rwi mor_function_cat1 H. rwi mor_function_cat2 H0. xd. rw mor_function_cat1; xd. Qed.
imports: Arith ordinal nat_trans