Definition is_univalent_reindex_twosided_disp_cat_help_to {x₁ : C₁} {y₁ : C₂} (xy₁ xy₂ : reindex_twosided_disp_cat x₁ y₁) (fg : 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. simple refine (_ ,, _ ,, _ ,, _). - exact (transportb (λ z, _ -->[ z ][ _] _) (functor_id _ _) (transportb (λ z, _ -->[ _ ][ z ] _) (functor_id _ _) (pr1 fg))). - exact (transportb (λ z, _ -->[ z ][ _] _) (functor_id _ _) (transportb (λ z, _ -->[ _ ][ z ] _) (functor_id _ _) (iso_inv_twosided_disp (pr2 fg)))). - abstract (cbn ; unfold transportb ; rewrite two_disp_pre_whisker_left ; rewrite two_disp_pre_whisker_right ; rewrite two_disp_post_whisker_left ; rewrite two_disp_post_whisker_right ; etrans ; [ apply twosided_prod_transport | ] ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; etrans ; [ apply maponpaths ;apply (inv_after_iso_twosided_disp (pr2 fg)) | ] ; unfold transportb ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; refine (!_) ; etrans ; [ apply twosided_prod_transport | ] ; apply maponpaths_2 ; apply isasetdirprod ; apply homset_property). - abstract (cbn ; unfold transportb ; rewrite two_disp_pre_whisker_left ; rewrite two_disp_pre_whisker_right ; rewrite two_disp_post_whisker_left ; rewrite two_disp_post_whisker_right ; etrans ; [ apply twosided_prod_transport | ] ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; etrans ; [ apply maponpaths ;apply (iso_after_inv_twosided_disp (pr2 fg)) | ] ; unfold transportb ; etrans ; [ apply maponpaths ; apply twosided_prod_transport | ] ; rewrite transport_f_f ; refine (!_) ; etrans ; [ apply twosided_prod_transport | ] ; 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.