Lemma isapropisunital {X : hSet} (opp : binop X) : isaprop (isunital opp). Proof. apply (@isapropsubtype X (λ un0, hconj (make_hProp _ (isapropislunit opp un0)) (make_hProp _ (isapropisrunit opp un0)))). intros u1 u2. intros ua1 ua2. apply (!(pr2 ua2 u1) @ (pr1 ua1 u2)). Defined.