proposition: Lemma is_mor_from_arrows2 : forall u, is_mor from_arrows u = inc u morphism_set.
proof: Proof. ir. ap iff_eq; ir. ufi from_arrows H. rwi is_mor_create H. am. uf from_arrows; rww is_mor_create. Qed.
imports: Arith ordinal nat_trans