Proposition right_beck_chevalley_nat_trans_id : right_beck_chevalley_nat_trans P P (fiber_functor_natural_nat_z_iso HD HD (id_cartesian_disp_functor D) f) a = identity _. Proof. rewrite right_beck_chevalley_nat_trans_id_on_ob. rewrite right_beck_chevalley_nat_trans_id_natural. rewrite functor_id. rewrite id_right. exact (pr222 P a). 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.