Proposition comm_nat_z_iso_inv_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_inv f g h k p φ = fiber_functor_from_cleaving_comp _ _ _ φ · fiber_functor_on_eq HD (!p) φ · fiber_functor_from_cleaving_comp_inv _ _ _ φ. Proof. cbn -[fiber_category fiber_functor_from_cleaving_comp]. apply maponpaths_2. apply maponpaths. induction p. cbn. apply idpath. 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.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.