(id0 id1 : forall x, morphism C x x) (id1_left : forall s d (m : morphism C s d), id1 _ o m = m) (id0_right : forall s d (m : morphism C s d), m o id0 _ = m) : id0 == id1. Proof. intro. etransitivity; [ symmetry; apply id1_left | apply id0_right ]. Qed.