Definition make_z_iso_in_fiber {xy₁ xy₂ : fiber_twosided_disp_cat} (f : z_iso xy₁ xy₂) : iso_twosided_disp (idtoiso (idpath x)) (idtoiso (idpath y)) xy₁ xy₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr1 f). - exact (inv_from_z_iso f). - abstract (cbn ; pose (p := z_iso_inv_after_z_iso f) ; cbn in p ; rewrite <- p ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite !twosided_swap_transport ; refine (!_) ; refine (transportbfinv (λ z, _ -->[ z ][ _ ] _) _ _ @ _) ; exact (transportbfinv (λ z, _ -->[ _ ][ z ] _) _ _)). - abstract (cbn ; pose (p := z_iso_after_z_iso_inv f) ; cbn in p ; rewrite <- p ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite !twosided_swap_transport ; refine (!_) ; refine (transportbfinv (λ z, _ -->[ z ][ _ ] _) _ _ @ _) ; exact (transportbfinv (λ z, _ -->[ _ ][ z ] _) _ _)). 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.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. 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.