Lemma weqlunitrunit {X : hSet} (opp : binop X) (is : iscomm opp) (un0 : X) : (islunit opp un0) ≃ (isrunit opp un0). Proof. assert (f : (islunit opp un0) → (isrunit opp un0)). { unfold islunit. unfold isrunit. intro isl. intro x. induction (is un0 x). apply (isl x). } assert (g : (isrunit opp un0) → (islunit opp un0)). { unfold islunit. unfold isrunit. intro isr. intro x. induction (is x un0). apply (isr x). } exists f. apply (isweqimplimpl f g (isapropislunit opp un0) (isapropisrunit opp un0)). Defined.