Proposition right_beck_chevalley_nat_trans_ob {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)) (x : C₂) : right_beck_chevalley_nat_trans HF HH τ x = η₂ (G(FR x)) · #HR(τ(FR x)) · #HR(#K(ε₁ 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.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.