Definition is_z_iso_cat_of_elems {cx₁ cx₂ : cat_of_elems} (f : cx₁ --> cx₂) (Hf : is_z_isomorphism (pr1 f)) : is_z_isomorphism f. Proof. use tpair. - simple refine (inv_from_z_iso (make_z_iso' _ Hf) ,, _). abstract (cbn ; pose (pr2 f) as p ; cbn in p ; rewrite <- p ; exact (eqtohomot (z_iso_inv_after_z_iso (functor_on_z_iso F (make_z_iso' _ Hf))) (pr2 cx₁))). - split. + abstract (use subtypePath ; [ intro ; apply (F _) | ] ; apply (z_iso_inv_after_z_iso (make_z_iso' _ Hf))). + abstract (use subtypePath ; [ intro ; apply (F _) | ] ; apply (z_iso_after_z_iso_inv (make_z_iso' _ Hf))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.