Definition left_beck_chevalley {w x y z : C} (f : x --> w) (g : y --> w) (h : z --> y) (k : z --> x) (p : k · f = h · g) (L₁ : dependent_sum f) (L₂ : dependent_sum h) : UU := ∏ (a : D[{x}]), is_z_isomorphism (left_beck_chevalley_nat_trans L₁ L₂ (comm_nat_z_iso f g h k p) a).
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.