Lemma weqlinvrinv {X : hSet} (opp : binop X) (is : iscomm opp) (un0 : X) (inv0 : X → X) : (islinv opp un0 inv0) ≃ (isrinv opp un0 inv0). Proof. assert (f : (islinv opp un0 inv0) → (isrinv opp un0 inv0)). { unfold islinv. unfold isrinv. intro isl. intro x. induction (is (inv0 x) x). apply (isl x). } assert (g : (isrinv opp un0 inv0) → (islinv opp un0 inv0)). { unfold islinv. unfold isrinv. intro isr. intro x. induction (is x (inv0 x)). apply (isr x). } exists f. apply (isweqimplimpl f g (isapropislinv opp un0 inv0) (isapropisrinv opp un0 inv0)). Qed.