Definition is_univalent_reindex_twosided_disp_cat (HD : is_univalent_twosided_disp_cat D) : is_univalent_twosided_disp_cat reindex_twosided_disp_cat. Proof. intros x₁ x₂ y₁ y₂ p q xy₁ xy₂. induction p ; induction q. use weqhomot. - exact (iso_weq_reindex_twosided_disp_cat _ _ xy₁ xy₂ ∘ is_univalent_reindex_twosided_disp_cat_help_weq xy₁ xy₂ ∘ make_weq _ (HD _ _ _ _ (idpath _) (idpath _) xy₁ xy₂))%weq. - abstract (intro p ; induction p ; 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.