Definition abmonoid_univalence_weq1 : abmonoid ≃ abmonoid' := weqtotal2asstol (λ X : setwithbinop, ismonoidop (@op X)) (λ y : (∑ X : setwithbinop, ismonoidop op), iscomm (@op (pr1 y))).
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.