Lemma isrigops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) : isrigops op1 op2 → isrigops (binop_weq_bck H op1) (binop_weq_bck H op2). Proof. intro is. split. - use tpair. + split. apply isabmonoidop_weq_bck, (pr1 (pr1 (pr1 is))). apply ismonoidop_weq_bck, (pr2 (pr1 (pr1 is))). + split ; simpl. * intros x. apply (maponpaths (invmap H)). refine (_ @ pr1 (pr2 (pr1 is)) _). apply (maponpaths (λ x, op2 x _)). apply homotweqinvweq. * intros x. apply (maponpaths (invmap H)). refine (_ @ pr2 (pr2 (pr1 is)) _). apply (maponpaths (op2 _)). apply homotweqinvweq. - apply isdistr_weq_bck, (pr2 is). Defined.