Definition from_is_iso_reindex_twosided_disp_cat : is_iso_twosided_disp (functor_on_is_z_isomorphism F Hf) (functor_on_is_z_isomorphism G Hg) fg. Proof. simple refine (_ ,, _ ,, _). - exact (iso_inv_twosided_disp Hfg). - abstract (cbn ; unfold transportb ; pose (p := inv_after_iso_twosided_disp Hfg) ; cbn in p ; rewrite twosided_prod_transportb in p ; pose (@transportf_transpose_right _ (λ z, _ -->[ pr1 z ][ dirprod_pr2 z ] _) _ _ (pathsdirprod _ _) _ _ p) as p' ; refine (p' @ _) ; unfold transportb_disp_mor2, transportf_disp_mor2, transportb ; cbn ; rewrite twosided_prod_transport_reindex ; rewrite !twosided_prod_transport ; rewrite !transport_f_f ; apply maponpaths_2 ; apply isaset_dirprod ; apply homset_property). - abstract (cbn ; unfold transportb ; pose (p := iso_after_inv_twosided_disp Hfg) ; cbn in p ; rewrite twosided_prod_transportb in p ; pose (@transportf_transpose_right _ (λ z, _ -->[ pr1 z ][ dirprod_pr2 z ] _) _ _ (pathsdirprod _ _) _ _ p) as p' ; refine (p' @ _) ; unfold transportb_disp_mor2, transportf_disp_mor2, transportb ; cbn ; rewrite twosided_prod_transport_reindex ; rewrite !twosided_prod_transport ; 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.