Lemma bin_hrel_z_iso_equiv_hset_z_iso_law' {X Y : hSet} (i : z_iso (C := REL) X Y) : function_to_bin_hrel (bin_hrel_is_z_iso_to_function (pr2 i)) = pr1 i. Proof. apply funextsec ; intro x. apply funextsec ; intro y. set (q := bin_hrel_is_z_iso_to_image_isaprop (pr2 i) x (bin_hrel_is_z_iso_to_image (pr2 i) x)). apply hPropUnivalence. - intro p. induction p. exact (pr2 (bin_hrel_is_z_iso_to_image (pr2 i) x)). - intro p. set (c := bin_hrel_is_z_iso_to_image_isaprop (pr2 i) x (bin_hrel_is_z_iso_to_image (pr2 i) x) (y,,p)). exact (base_paths _ _ (pr1 c)). Qed.
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.