Lemma isrdistr_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) : isrdistr op1 op2 → isrdistr (binop_weq_fwd H op1) (binop_weq_fwd H op2). Proof. intros is x y z. unfold binop_weq_fwd. apply maponpaths. refine (_ @ is _ _ _ @ _). - apply (maponpaths (λ x, op2 x _)). apply homotinvweqweq. - apply map_on_two_paths ; apply homotinvweqweq0. Defined.