proposition: 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: 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 (pathscomp0 _ (pr1 (pr2 (pr1 is)) _)). apply (maponpaths (λ x, op2 x _)). apply homotweqinvweq. * intros x. apply (maponpaths (invmap H)). refine (pathscomp0 _ (pr2 (pr2 (pr1 is)) _)). apply (maponpaths (op2 _)). apply homotweqinvweq. - apply isdistr_weq_bck, (pr2 is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions