proposition: Lemma weqlunitrunit {X : hSet} (opp : binop X) (is : iscomm opp) (un0 : X) : (islunit opp un0) ≃ (isrunit opp un0).
proof: Proof. assert (f : (islunit opp un0) -> (isrunit opp un0)). { unfold islunit. unfold isrunit. intro isl. intro x. destruct (is un0 x). apply (isl x). } assert (g : (isrunit opp un0) -> (islunit opp un0)). { unfold islunit. unfold isrunit. intro isr. intro x. destruct (is x un0). apply (isr x). } split with f. apply (isweqimplimpl f g (isapropislunit opp un0) (isapropisrunit opp un0)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions