proposition: Lemma mor_from_arrows : forall u, mor from_arrows u = (ob from_arrows (source u) & ob from_arrows (target u) & inc u (homs (source u) (target u))).
proof: Proof. ir. cp from_arrows_axioms. ap iff_eq; ir. assert (is_mor from_arrows u). app mor_is_mor. rwi is_mor_from_arrows H1. ee; try am. app is_ob_ob. app is_ob_ob. ap is_mor_mor. ap from_arrows_axioms. rww is_mor_from_arrows. ee; try am. app ob_is_ob. app ob_is_ob. Qed.
imports: Arith ordinal nat_trans