Lemma monoid_univalence_isweq (X Y : monoid) : isweq (monoid_univalence_map X Y). 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. refine (weqcomp_to_funcomp_app @ _). use weqcomp_to_funcomp_app. - use weqproperty. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.