Lemma binop_iso_equiv (A B : ob BINOP) : z_iso A B -> binopiso A B. Proof. intro f. use make_binopiso. set (X := binop_iso_is_equiv A B f). apply (make_weq (pr1 (pr1 f)) X). apply (pr2 (pr1 f)). 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.