proposition: Lemma isrdistr_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) : isrdistr op1 op2 → isrdistr (binop_weq_bck H op1) (binop_weq_bck H op2).
proof: Proof. intros is x y z. unfold binop_weq_bck. apply maponpaths. refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)). - apply (maponpaths (λ x, op2 x _)). apply homotweqinvweq. - apply map_on_two_paths ; apply pathsinv0, homotweqinvweq. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions