Lemma binop_equiv_is_z_iso (A B : setwithbinop) (f : binopiso A B) : @is_z_isomorphism BINOP A B (make_binopfun (pr1 (pr1 f)) (pr2 f)). Proof. exists (make_binopfun (pr1 (pr1 (invbinopiso f))) (pr2 (invbinopiso f))). split; cbn. - unfold compose, identity. cbn. unfold binopfuncomp, idbinopfun. cbn. use total2_paths_f. cbn. apply funextfun. intros x. apply homotinvweqweq. cbn. apply impred_isaprop. intros t. apply impred_isaprop. intros t0. apply (pr2 (pr1 A)). - use total2_paths_f. cbn. apply funextfun. intros x. apply homotweqinvweq. cbn. apply impred_isaprop. intros yt. apply impred_isaprop. intros t0. apply (pr2 (pr1 B)). 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.