Definition iso_weq_reindex_twosided_disp_cat {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : x₁ --> x₂} (Hf : is_z_isomorphism f) {g : y₁ --> y₂} (Hg : is_z_isomorphism g) (xy₁ : D (F x₁) (G y₁)) (xy₂ : D (F x₂) (G y₂)) : @iso_twosided_disp _ _ D _ _ _ _ (#F f ,, functor_on_is_z_isomorphism F Hf) (#G g ,, functor_on_is_z_isomorphism G Hg) xy₁ xy₂ ≃ @iso_twosided_disp _ _ reindex_twosided_disp_cat _ _ _ _ (f ,, Hf) (g ,, Hg) xy₁ xy₂. Proof. use weq_iso. - exact (λ fg, iso_reindex_twosided_disp_cat Hf Hg (pr2 fg)). - exact (λ fg, iso_from_is_iso_reindex_twosided_disp_cat Hf Hg (pr2 fg)). - abstract (intro fg ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; apply idpath). - abstract (intro fg ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; 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.Core.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromReindexIso. End FromReindexIso.