Lemma setwith2binop_equiv_is_z_iso (X Y : ob setwith2binop_category) (f : twobinopiso X Y) : @is_z_isomorphism setwith2binop_precategory X Y (make_twobinopfun (pr1 (pr1 f)) (pr2 f)). Proof. exists (make_twobinopfun (pr1 (pr1 (invtwobinopiso f))) (pr2 (invtwobinopiso f))). split. - use twobinopfun_paths. use funextfun. intros x. use homotinvweqweq. - use twobinopfun_paths. use funextfun. intros y. use homotweqinvweq. 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.