Definition bin_hrel_z_iso_equiv_hset_z_iso (X Y : hSet) : z_iso (C := HSET) X Y ≃ z_iso (C := REL) X Y. Proof. use weq_iso. - exact (λ i, z_iso_in_SET_to_z_iso_in_REL i). - exact (λ i, bin_hrel_is_z_iso_to_equality (pr2 i)). - intro ; apply z_iso_eq, bin_hrel_z_iso_equiv_hset_z_iso_law. - intro ; apply z_iso_eq, bin_hrel_z_iso_equiv_hset_z_iso_law'. 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.