Lemma setwith2binop_univalence_isweq (X Y : setwith2binop) : isweq (setwith2binop_univalence_map X Y). Proof. use isweqhomot. - exact (weqcomp (setwith2binop_univalence_weq1 X Y) (setwith2binop_univalence_weq2 X Y)). - intros e. induction e. use weqcomp_to_funcomp_app. - use weqproperty. Defined.