Definition bin_hrel_is_z_iso_to_equality {X Y : hSet} {r : bin_hrel X Y} (p : is_z_isomorphism (C := REL) r) : z_iso (C := HSET) X Y. Proof. set (j := (r ,, p : z_iso (C := REL) X Y)). set (i := is_z_iso_inv_from_z_iso j). use make_z_iso. - exact (bin_hrel_is_z_iso_to_function p). - exact (bin_hrel_is_z_iso_to_function i). - abstract (split ; (apply funextsec ; intro) ; [ apply bin_hrel_is_z_iso_to_equality_inverse_law | apply (bin_hrel_is_z_iso_to_equality_inverse_law i)]). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.All.