Definition disp_nat_z_iso_inv {α: nat_z_iso F G} (β :disp_nat_z_iso DF DG α) : disp_nat_z_iso DG DF (nat_z_iso_inv α). Proof. use tpair. - exact (disp_nat_z_iso_to_trans_inv β). - intros c d. exists (β c d). split. * exact (pr2 (pr2 (pr2 β c d))). * exact (pr1 (pr2 (pr2 β c d))). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.