proposition: Lemma monoid_univalence_isweq (X Y : monoid) : isweq (monoid_univalence_map X Y).
proof: Proof. use isweqhomot. - exact (weqcomp (monoid_univalence_weq1 X Y) (weqcomp (monoid_univalence_weq2 X Y) (monoid_univalence_weq3 X Y))). - intros e. induction e. use (pathscomp0 weqcomp_to_funcomp_app). use weqcomp_to_funcomp_app. - use weqproperty. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders