Definition from_iso_right_total_of_twosided_disp_cat_pr2 {x : C₁} {xy₁ xy₂ : right_total_of_twosided_disp_cat x} (g : z_iso_disp (identity_z_iso _) xy₁ xy₂) : iso_twosided_disp (identity_z_iso _) (from_iso_right_total_of_twosided_disp_cat_pr1 g) (pr2 xy₁) (pr2 xy₂). Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr21 g). - exact (pr212 g). - abstract (pose (p := inv_mor_after_z_iso_disp g) ; unfold mor_disp in p ; cbn in p ; rewrite transportb_total2 in p ; refine (!(fiber_paths (!p)) @ _) ; cbn ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite twosided_swap_transport ; rewrite !twosided_prod_transport ; apply maponpaths_2 ; apply isaset_dirprod ; apply homset_property). - abstract (pose (p := z_iso_disp_after_inv_mor g) ; unfold mor_disp in p ; cbn in p ; rewrite transportb_total2 in p ; refine (!(fiber_paths (!p)) @ _) ; cbn ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite twosided_swap_transport ; rewrite !twosided_prod_transport ; 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Section FromIsoTotal. End FromIsoTotal.