Proposition left_beck_chevalley_nat_trans_ob {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)) (x : C₂) : left_beck_chevalley_nat_trans HF HH τ x = #HL (#K (η₁ x)) · #HL (τ (FL x)) · ε₂ (G (FL x)). 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.