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