Lemma nat_trafo_pointwise_z_iso_if_z_iso {C : precategory_data} {C' : precategory} (hs: has_homsets C') {F G : ob [C, C', hs]} (α : F --> G) : is_z_isomorphism α -> is_nat_z_iso (pr1 α). Proof. intro H. red. intro c. set (αcinv := pr1 (inv_from_z_iso (α,,H)) c). use make_is_z_isomorphism. - exact αcinv. - assert (HH := is_z_isomorphism_is_inverse_in_precat H). induction HH as [HH1 HH2]. apply (maponpaths pr1) in HH1. apply toforallpaths in HH1. apply (maponpaths pr1) in HH2. apply toforallpaths in HH2. split. + apply HH1. + apply HH2. Defined.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence.