Definition to_iso_set_rel_disp_cat {X Y : SET} (R₁ R₂ : set_rel_disp_cat X Y) (f : ∏ (x : pr1 X) (y : pr1 Y), R₁ x y ≃ R₂ x y) : iso_twosided_disp (identity_z_iso X) (identity_z_iso Y) R₁ R₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (λ x y, f x y). - exact (λ x y, invmap (f x y)). - abstract (cbn ; use funextsec ; intro x ; use funextsec ; intro y ; use funextsec ; intro r ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite transportf_set_rel ; refine (!_) ; do 2 (refine (transportf_id_left _ _ _ _ @ _)) ; exact (!(homotinvweqweq (f x y) r))). - abstract (cbn ; use funextsec ; intro x ; use funextsec ; intro y ; use funextsec ; intro r ; unfold transportb_disp_mor2, transportf_disp_mor2 ; cbn ; rewrite transportf_set_rel ; refine (!_) ; do 2 (refine (transportf_id_left _ _ _ _ @ _)) ; exact (!(homotweqinvweq (f x y) r))). 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.