Lemma weqlinvertiblerinvertible {X : UU} (opp : binop X) (is : iscomm opp) (x : X) : (islinvertible opp x) ≃ (isrinvertible opp x). Proof. assert (f : (islinvertible opp x) → (isrinvertible opp x)). { unfold islinvertible. unfold isrinvertible. intro isl. apply (isweqhomot (λ y, opp x y)). - intro z. apply is. - apply isl. } assert (g : (isrinvertible opp x) → (islinvertible opp x)). { unfold islinvertible. unfold isrinvertible. intro isr. apply (λ h, isweqhomot _ _ h isr). intro x0. apply is. } exists f. apply (isweqimplimpl f g (isapropisweq (λ x0 : X, opp x x0)) (isapropisweq (λ x0 : X, opp x0 x))). Defined.