Definition monoid_univalence_weq3 (X Y : monoid) : (monoidiso' X Y) ≃ (monoidiso X Y) := weqtotal2asstor (λ w : X ≃ Y, isbinopfun w) (λ y : (∑ w : weq X Y, isbinopfun w), (pr1 y) 1 = 1).
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.