Lemma setwith2binop_iso_is_equiv (A B : ob setwith2binop_category) (f : z_iso A B) : isweq (pr1 (pr1 f)). Proof. use isweq_iso. - exact (pr1twobinopfun _ _ (inv_from_z_iso f)). - intros x. use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_inv_after_z_iso f)) x). intros x0. use isapropistwobinopfun. - intros x. use (toforallpaths _ _ _ (subtypeInjectivity _ _ _ _ (z_iso_after_z_iso_inv f)) x). intros x0. use isapropistwobinopfun. 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.