proposition: Lemma mor_function_cat2 : forall z u, mor (function_cat z) u = (Arrow.like u & inc (source u) z & inc (target u) z & Map.axioms (source u) (target u) (arrow u)).
proof: Proof. ir. rw mor_function_cat1. ap iff_eq; ir; xd. rwi inc_function_arrow_set H2; ee; am. rw inc_function_arrow_set. ee; try am. tv. tv. uh H2; ee; am. uh H2; ee; am. uh H2; ee; am. Qed.
imports: Arith ordinal nat_trans