Definition reindex_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp reindex_twosided_disp_cat_ob_mor. Proof. simple refine (_ ,, _). - exact (λ x y xy, transportb (λ z, _ -->[ z ][ _] _) (functor_id _ _) (transportb (λ z, _ -->[ _ ][ z ] _) (functor_id _ _) (id_two_disp _))). - exact (λ x₁ x₂ x₃ y₁ y₂ y₃ xy₁ xy₂ xy₃ f₁ f₂ g₁ g₂ fg₁ fg₂, transportb (λ z, _ -->[ z ][ _] _) (functor_comp _ _ _) (transportb (λ z, _ -->[ _ ][ z ] _) (functor_comp _ _ _) (fg₁ ;;2 fg₂))). 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.