proposition: Lemma isringops_weq_bck {X Y : UU} (H : X ≃ Y) (op1 op2 : binop Y) : isringops op1 op2 → isringops (binop_weq_bck H op1) (binop_weq_bck H op2).
proof: Proof. intro is. split. - split. + apply isabgrop_weq_bck, (pr1 (pr1 is)). + apply ismonoidop_weq_bck, (pr2 (pr1 is)). - apply isdistr_weq_bck, (pr2 is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions