Lemma binop_iso_is_equiv (A B : ob BINOP) (f : z_iso A B) : isweq (pr1 (pr1 f)). Proof. apply (isweq_iso _ (pr1binopfun _ _ (inv_from_z_iso f))). - intro x. set (T:=z_iso_inv_after_z_iso f). apply subtypeInjectivity in T. set (T':=toforallpaths _ _ _ T). apply T'. intro x0. apply isapropisbinopfun. - intros y. set (T:=z_iso_after_z_iso_inv f). apply subtypeInjectivity in T. set (T':=toforallpaths _ _ _ T). apply T'. intros x0. apply isapropisbinopfun. 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. Require Import UniMath.CategoryTheory.Core.Functors.