proposition: Lemma left_id_from_arrows : forall u, is_mor from_arrows u -> comp from_arrows (id from_arrows (target u)) u = u.
proof: Proof. ir. cp property_hyp. cp H. rwi is_mor_from_arrows H1. ee. cp H1; cp H2. rwi is_ob_from_arrows H4; rwi is_ob_from_arrows H5. rww comp_from_arrows. rww id_from_arrows. uh H0; ee. apply H11 with (source u). am. am. am. app is_mor_id_from_arrows. rww source_id_from_arrows. Qed.
imports: Arith ordinal nat_trans