Definition comm_nat_z_iso_inv {w x y z : C} (f : x --> w) (g : y --> w) (h : z --> y) (k : z --> x) (p : k · f = h · g) (F := fiber_functor_from_cleaving D HD f : D[{w}] ⟶ D[{x}]) (G := fiber_functor_from_cleaving D HD g : D[{w}] ⟶ D[{y}]) (H := fiber_functor_from_cleaving D HD h : D[{y}] ⟶ D[{z}]) (K := fiber_functor_from_cleaving D HD k : D[{x}] ⟶ D[{z}]) : nat_z_iso (G ∙ H) (F ∙ K) := nat_z_iso_inv (comm_nat_z_iso HD f g h k p).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.