Definition is_z_iso_pointed_sets {X Y : pointed_sets} (f : X --> Y) (Hf : is_z_isomorphism (pr1 f)) : is_z_isomorphism f. Proof. use tpair. - simple refine (_ ,, _). + exact (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 (make_z_iso' _ Hf)) (pr2 X))). - split. + abstract (use subtypePath ; [ intro ; apply (pr1 X) | ] ; exact (z_iso_inv_after_z_iso (make_z_iso' _ Hf))). + abstract (use subtypePath ; [ intro ; apply (pr1 Y) | ] ; exact (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.