Definition comm_nat_z_iso {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 (F ∙ K) (G ∙ H) := nat_z_iso_comp (fiber_functor_from_cleaving_comp_nat_z_iso _ _ _) (nat_z_iso_comp (fiber_functor_on_eq_nat_z_iso HD p) (nat_z_iso_inv (fiber_functor_from_cleaving_comp_nat_z_iso _ _ _))).
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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Pullbacks.