Definition make_iso_right_total_of_twosided_disp_cat {x : C₁} {xy₁ xy₂ : right_total_of_twosided_disp_cat x} (g : z_iso (pr1 xy₁) (pr1 xy₂)) (fg : iso_twosided_disp (identity_z_iso _) g (pr2 xy₁) (pr2 xy₂)) : z_iso_disp (identity_z_iso _) xy₁ xy₂. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact (pr1 g ,, pr1 fg). - exact (pr12 g ,, pr12 fg). - abstract (unfold mor_disp ; cbn ; rewrite transportb_total2 ; cbn ; use total2_paths_f ; [ apply z_iso_after_z_iso_inv | ] ; cbn ; etrans ; [ apply maponpaths ; apply (iso_after_inv_twosided_disp (pr2 fg)) | ] ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite <- twosided_swap_transport ; apply transportfbinv). - abstract (unfold mor_disp ; cbn ; rewrite transportb_total2 ; cbn ; use total2_paths_f ; [ apply z_iso_inv_after_z_iso | ] ; cbn ; etrans ; [ apply maponpaths ; apply (inv_after_iso_twosided_disp (pr2 fg)) | ] ; unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ; rewrite <- twosided_swap_transport ; apply transportfbinv). 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.