proposition: Lemma weqldistrrdistr {X : hSet} (opp1 opp2 : binop X) (is : iscomm opp2) : (isldistr opp1 opp2) ≃ (isrdistr opp1 opp2).
proof: Proof. assert (f : (isldistr opp1 opp2) -> (isrdistr opp1 opp2)). { unfold isldistr. unfold isrdistr. intro isl. intros x x' x''. destruct (is x'' (opp1 x x')). destruct (is x'' x). destruct (is x'' x'). apply (isl x x' x''). } assert (g : (isrdistr opp1 opp2) -> (isldistr opp1 opp2)). { unfold isldistr. unfold isrdistr. intro isr. intros x x' x''. destruct (is (opp1 x x') x''). destruct (is x x''). destruct (is x' x''). apply (isr x x' x''). } split with f. apply (isweqimplimpl f g (isapropisldistr opp1 opp2) (isapropisrdistr opp1 opp2)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions