proposition: Lemma setwithbinop_univalence_isweq (X Y : setwithbinop) : isweq (setwithbinop_univalence_map X Y).
proof: Proof. use isweqhomot. - exact (weqcomp (setwithbinop_univalence_weq1 X Y) (setwithbinop_univalence_weq2 X Y)). - intros e. induction e. use weqcomp_to_funcomp_app. - use weqproperty. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions