proposition: Lemma inverse_swap_relation {X Y : hSet} {r : bin_hrel X Y} (i : is_z_isomorphism (C := REL) r) : ∏ (x : X) (y : Y), r x y -> pr1 i y x.
proof: Proof. intros x y p. set (t := eqtohomot (eqtohomot (pr12 i) x) x). set (q := path_to_fun (X := eqset x x) (! (base_paths _ _ t)) (idpath x)). use (factor_through_squash_hProp _ _ q). clear q ; intro q. assert (q0 : pr1 q = y). { set (ty := eqtohomot (eqtohomot (pr22 i) (pr1 q)) y). use (path_to_fun (base_paths _ _ ty)). apply hinhpr. exists x. split. - exact (pr22 q). - exact p. } induction q0. exact (pr22 q). 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