Definition left_beck_chevalley_nat_trans {C₁ C₂ C₃ C₄ : category} {F : C₁ ⟶ C₂} {G : C₁ ⟶ C₃} {H : C₃ ⟶ C₄} {K : C₂ ⟶ C₄} (HF : is_right_adjoint F) (FL := left_adjoint HF) (η₁ := unit_from_right_adjoint HF) (HH : is_right_adjoint H) (HL := left_adjoint HH) (ε₂ := counit_from_right_adjoint HH) (τ : nat_z_iso (F ∙ K) (G ∙ H)) : K ∙ HL ⟹ FL ∙ G := nat_trans_comp _ _ _ (post_whisker η₁ (K ∙ HL)) (nat_trans_comp _ _ _ (pre_whisker FL (post_whisker τ HL)) (pre_whisker (FL ∙ G) ε₂)).
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.