Definition from_iso_set_rel_disp_cat {X Y : SET} (R₁ R₂ : set_rel_disp_cat X Y) (f : iso_twosided_disp (identity_z_iso X) (identity_z_iso Y) R₁ R₂) (x : pr1 X) (y : pr1 Y) : R₁ x y ≃ R₂ x y. Proof. use weq_iso. - exact (pr1 f x y). - exact (pr12 f x y). - abstract (intros r ; pose (p := eqtohomot (eqtohomot (eqtohomot (pr122 f) x) y) r) ; refine (p @ _) ; cbn ; clear p ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite transportf_set_rel ; do 2 (refine (transportf_id_left _ _ _ _ @ _)) ; apply idpath). - abstract (intros r ; pose (p := eqtohomot (eqtohomot (eqtohomot (pr222 f) x) y) r) ; refine (p @ _) ; cbn ; clear p ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite transportf_set_rel ; do 2 (refine (transportf_id_left _ _ _ _ @ _)) ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration.