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. 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.
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.