fact: Definition pointwise_z_iso_from_nat_z_iso {A X : precategory} {hsX : has_homsets X} {F G : functor_precategory A X hsX} (b : z_iso F G) (a : A) : z_iso (pr1 F a) (pr1 G a) := functor_z_iso_pointwise_if_z_iso _ _ _ _ _ b (pr2 b)_ .
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing