Lemma nat_trans_inv_pointwise_inv_after_p_z_iso (C : precategory_data) (C' : precategory) (hs: has_homsets C') (F G : ob [C, C', hs]) (A : F --> G) (Aiso: is_z_isomorphism A) a : inv_from_z_iso (functor_z_iso_pointwise_if_z_iso C C' hs F G A Aiso a) = pr1 (inv_from_z_iso (A,, Aiso)) a. Proof. apply idpath. Qed.
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.