Definition is_iso_reindex_twosided_disp_cat : @is_iso_twosided_disp _ _ reindex_twosided_disp_cat _ _ _ _ _ _ _ _ Hf Hg fg. Proof. simple refine (_ ,, _ ,, _). - exact (iso_inv_twosided_disp Hfg). - abstract (cbn ; unfold transportb_disp_mor2, transportf_disp_mor2, transportb ; cbn ; etrans ; [ apply twosided_prod_transport | ] ; etrans ; [ apply maponpaths ; exact (inv_after_iso_twosided_disp Hfg) | ] ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; refine (!_) ; etrans ; [ do 2 apply maponpaths ; apply twosided_prod_transport | ] ; etrans ; [ apply twosided_prod_transport_reindex | ] ; rewrite transport_f_f ; apply maponpaths_2 ; apply isaset_dirprod ; apply homset_property). - abstract (cbn ; unfold transportb_disp_mor2, transportf_disp_mor2, transportb ; cbn ; etrans ; [ apply twosided_prod_transport | ] ; etrans ; [ apply maponpaths ; exact (iso_after_inv_twosided_disp Hfg) | ] ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; refine (!_) ; etrans ; [ do 2 apply maponpaths ; apply twosided_prod_transport | ] ; etrans ; [ apply twosided_prod_transport_reindex | ] ; rewrite transport_f_f ; apply maponpaths_2 ; apply isaset_dirprod ; apply homset_property). 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.