proposition: Lemma weqlinvertiblerinvertible {X : UU} (opp : binop X) (is : iscomm opp) (x : X) : (islinvertible opp x) ≃ (isrinvertible opp x).
proof: 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. } split with f. apply (isweqimplimpl f g (isapropisweq (λ x0 : X, opp x x0)) (isapropisweq (λ x0 : X, opp x0 x))). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions