Definition setwith2binop_category_isweq (X Y : ob setwith2binop_category) : isweq (λ p : X = Y, idtoiso p). Proof. use (@isweqhomot (X = Y) (z_iso X Y) (pr1weq (weqcomp (setwith2binop_univalence X Y) (setwith2binop_equiv_weq_iso X Y))) _ _ (weqproperty (weqcomp (setwith2binop_univalence X Y) (setwith2binop_equiv_weq_iso X Y)))). intros e. induction e. use (pathscomp0 weqcomp_to_funcomp_app). use total2_paths_f. - use idpath. - use proofirrelevance. use isaprop_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence.