Proposition comm_nat_z_iso_ob {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}]) (φ : D[{w}]) : comm_nat_z_iso f g h k p φ = fiber_functor_from_cleaving_comp _ _ _ φ · fiber_functor_on_eq HD p φ · fiber_functor_from_cleaving_comp_inv _ _ _ φ. Proof. apply assoc. Qed.
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.