proposition: Lemma isapropisunital {X : hSet} (opp : binop X) : isaprop (isunital opp).
proof: Proof. apply (@isapropsubtype X (λ un0 : _, hconj (make_hProp _ (isapropislunit opp un0)) (make_hProp _ (isapropisrunit opp un0)))). intros u1 u2. intros ua1 ua2. apply (pathscomp0 (pathsinv0 (pr2 ua2 u1)) (pr1 ua1 u2)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions