proposition: Lemma isrigops_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) : isrigops op1 op2 → isrigops (binop_weq_fwd H op1) (binop_weq_fwd H op2).
proof: Proof. intro is. split. - use tpair. + split. apply isabmonoidop_weq_fwd, (pr1 (pr1 (pr1 is))). apply ismonoidop_weq_fwd, (pr2 (pr1 (pr1 is))). + split ; simpl. * intros x. apply (maponpaths H). refine (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)). apply (maponpaths (λ x, op2 x _)). apply homotinvweqweq. * intros x. apply (maponpaths H). refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)). apply (maponpaths (op2 _)). apply homotinvweqweq. - apply isdistr_weq_fwd, (pr2 is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions