Definition is_univalent_reindex_twosided_disp_cat_help_weq {x₁ : C₁} {y₁ : C₂} (xy₁ xy₂ : reindex_twosided_disp_cat x₁ y₁) : iso_twosided_disp (identity_z_iso (F x₁)) (identity_z_iso (G y₁)) xy₁ xy₂ ≃ iso_twosided_disp (_ ,, functor_on_is_z_isomorphism F (identity_is_z_iso x₁)) (_ ,, functor_on_is_z_isomorphism G (identity_is_z_iso y₁)) xy₁ xy₂. Proof. use weq_iso. - exact (is_univalent_reindex_twosided_disp_cat_help_to xy₁ xy₂). - exact (is_univalent_reindex_twosided_disp_cat_help_from xy₁ xy₂). - abstract (intros f ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; cbn in * ; unfold transportb ; rewrite !twosided_prod_transport ; rewrite transport_f_f ; refine (_ @ @idpath_transportf _ (λ z, xy₁ -->[ pr1 z ][ dirprod_pr2 z ] xy₂) (_ ,, _) (pr1 f)) ; apply maponpaths_2 ; apply isasetdirprod ; apply homset_property). - abstract (intros f ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; cbn in * ; unfold transportb ; rewrite !twosided_prod_transport ; rewrite transport_f_f ; refine (_ @ @idpath_transportf _ (λ z, xy₁ -->[ pr1 z ][ dirprod_pr2 z ] xy₂) (_ ,, _) (pr1 f)) ; apply maponpaths_2 ; apply isasetdirprod ; 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.