Lemma weqlcancelablercancelable {X : UU} (opp : binop X) (is : iscomm opp) (x : X) : (islcancelable opp x) ≃ (isrcancelable opp x). Proof. assert (f : (islcancelable opp x) → (isrcancelable opp x)). { unfold islcancelable. unfold isrcancelable. intro isl. apply (λ h, isinclhomot _ _ h isl). intro x0. apply is. } assert (g : (isrcancelable opp x) → (islcancelable opp x)). { unfold islcancelable. unfold isrcancelable. intro isr. apply (λ h, isinclhomot _ _ h isr). intro x0. apply is. } exists f. apply (isweqimplimpl f g (isapropisincl (λ x0 : X, opp x x0)) (isapropisincl (λ x0 : X, opp x0 x))). Defined.