proposition: Lemma is_mor_from_arrows : forall u, is_mor from_arrows u = (is_ob from_arrows (source u) & is_ob from_arrows (target u) & inc u (homs (source u) (target u))).
proof: Proof. ir. ap iff_eq; ir. ufi from_arrows H. rwi is_mor_create H. rwi inc_morphism_set H. xd. rww is_ob_from_arrows. rww is_ob_from_arrows. uf from_arrows; rw is_mor_create. rw inc_morphism_set. xd. rwi is_ob_from_arrows H; am. rwi is_ob_from_arrows H0; am. Qed.
imports: Arith ordinal nat_trans