proposition: Lemma mor_umorphism_cat : forall z u, mor (umorphism_cat z) u = (Umorphism.strong_axioms u & inc (source u) z & inc (target u) z).
proof: Proof. ir. cp (umorphism_cat_property z). uf umorphism_cat. rww mor_from_arrows. ap iff_eq; ir. ee. rwi inc_umorphism_set H2; ee; am. rwi ob_from_arrows H0. am. am. rwi ob_from_arrows H1; am. ee. rww ob_from_arrows. rww ob_from_arrows. rww inc_umorphism_set. ee; try am. tv. tv. Qed.
imports: Arith ordinal nat_trans