Definition is_z_iso_total {C : category} {D : disp_cat C} {xx yy : total_category D} (ff : xx --> yy) (i : is_z_isomorphism (pr1 ff)) (fi := pr1 ff,, i) (ii : is_z_iso_disp fi (pr2 ff)) : is_z_isomorphism ff. Proof. exists (inv_from_z_iso fi,, pr1 ii). abstract ( refine (total2_paths_f _ _ ,, total2_paths_f _ _); [ exact (maponpaths _ (inv_mor_after_z_iso_disp ii) @ transportfbinv _ _ _) | exact (maponpaths _ (z_iso_disp_after_inv_mor ii) @ transportfbinv _ _ _) ] ). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.