Lemma right_beck_chevalley_nat_trans_id_natural : fiber_functor_natural_nat_z_iso HD HD (id_cartesian_disp_functor D) f (R a) = identity _. Proof. cbn. use (cartesian_factorisation_unique (disp_functor_identity_is_cartesian_disp_functor D y x f (R a) (HD y x f (R a)) (HD y x f (R a)) (HD y x f (R a)))). rewrite cartesian_factorisation_commutes. cbn. rewrite id_left_disp. unfold transportb. apply maponpaths_2. apply homset_property. 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.