proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.Algebra.BinaryOperations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors