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