Lemma invertiblefunction_to_invertiblerelation_laws {X Y : hSet} {f : X → Y} (i : is_z_isomorphism (C := HSET) f) : (function_to_bin_hrel f : REL⟦_,_⟧) · function_to_bin_hrel (pr1 i) = identity (C := REL) X. Proof. apply funextsec ; intro x1. apply funextsec ; intro x2. use hPropUnivalence. + intro q. use (factor_through_squash_hProp (eqset x1 x2) _ q). clear q ; intro q. refine (! eqtohomot (pr12 i) x1 @ _ @ pr22 q). apply (maponpaths (pr1 i)). exact (pr12 q). + intro p ; induction p. apply hinhpr. exact (f x1 ,, idpath _ ,, eqtohomot (pr12 i) x1). 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.