Lemma right_beck_chevalley_nat_trans_id_on_ob : right_beck_chevalley_nat_trans P P (fiber_functor_natural_nat_z_iso HD HD (id_cartesian_disp_functor D) f) a = η (R a) · #R (fiber_functor_natural_nat_z_iso HD HD (id_cartesian_disp_functor D) f (R a)) · #R (ε a). Proof. rewrite right_beck_chevalley_nat_trans_ob. apply idpath. 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.