proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.HSET.All