Definition monoid_univalence_weq2 (X Y : monoid) : (X ╝ Y) ≃ (monoidiso' X Y). Proof. use weqbandf. - exact (setwithbinop_univalence X Y). - intros e. cbn. use invweq. induction X as [X Xop]. induction Y as [Y Yop]. cbn in e. cbn. induction e. use weqimplimpl. + intros i. use proofirrelevance. use isapropismonoidop. + intros i. induction i. use idpath. + use setproperty. + use isapropifcontr. exact (@isapropismonoidop X (pr2 X) Xop Yop). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.