Lemma fiber_functor_natural_comp : fiber_functor_natural HD₁ HD₃ (comp_cartesian_disp_functor FF GG) f (R₁ a) = fiber_functor_natural HD₂ HD₃ GG (#F f) (FF _ (R₁ a)) · #(fiber_functor GG (F x)) (fiber_functor_natural HD₁ HD₂ FF f (R₁ a)). Proof. cbn. use (cartesian_factorisation_unique (disp_functor_composite_is_cartesian_disp_functor (cartesian_disp_functor_is_cartesian FF) (cartesian_disp_functor_is_cartesian GG) 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. refine (!_). etrans. { rewrite mor_disp_transportf_prewhisker. rewrite !mor_disp_transportf_postwhisker. rewrite !transport_f_f. cbn. rewrite assoc_disp_var. rewrite transport_f_f. rewrite <- (disp_functor_comp_var GG). rewrite cartesian_factorisation_commutes. rewrite disp_functor_transportf. rewrite !mor_disp_transportf_prewhisker. rewrite !transport_f_f. rewrite cartesian_factorisation_commutes. rewrite !transport_f_f. apply idpath. } 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.