Definition pointwise_inv_is_inv_on_z_iso {A : precategory} {X : category} {F G : [A, X]} (b : z_iso F G) (a : A) : inv_from_z_iso (pointwise_z_iso_from_nat_z_iso b a) = pr1 (inv_from_z_iso b) a. Proof. apply idpath. Defined.
Require Import UniMath.Foundations.Sets. 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.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.