proposition: 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: Proof. apply assoc. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Pullbacks