Definition right_beck_chevalley_nat_trans {C₁ C₂ C₃ C₄ : category} {F : C₁ ⟶ C₂} {G : C₁ ⟶ C₃} {H : C₃ ⟶ C₄} {K : C₂ ⟶ C₄} (HF : is_left_adjoint F) (FR := right_adjoint HF) (ε₁ := counit_from_left_adjoint HF) (HH : is_left_adjoint H) (HR := right_adjoint HH) (η₂ := unit_from_left_adjoint HH) (τ : nat_z_iso (G ∙ H) (F ∙ K)) : FR ∙ G ⟹ K ∙ HR := nat_trans_comp _ _ _ (pre_whisker (FR ∙ G) η₂) (nat_trans_comp _ _ _ (post_whisker (pre_whisker FR τ) HR) (post_whisker ε₁ (K ∙ HR))).
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.