Proposition right_beck_chevalley_nat_trans_comp : right_beck_chevalley_nat_trans P₁ P₃ (fiber_functor_natural_nat_z_iso HD₁ HD₃ (comp_cartesian_disp_functor FF GG) f) a = #(fiber_functor GG _) (right_beck_chevalley_nat_trans P₁ P₂ (fiber_functor_natural_nat_z_iso HD₁ HD₂ FF f) a) · right_beck_chevalley_nat_trans P₂ P₃ (fiber_functor_natural_nat_z_iso HD₂ HD₃ GG (#F f)) (FF _ a). Proof. rewrite right_beck_chevalley_nat_trans_comp_ob. rewrite right_beck_chevalley_nat_trans_comp_ob_on_left. rewrite right_beck_chevalley_nat_trans_comp_ob_on_right. refine (!_). etrans. { rewrite !assoc. do 2 apply maponpaths_2. apply right_beck_chevalley_nat_trans_comp_natural. } rewrite !assoc'. apply maponpaths. refine (_ @ functor_comp R₃ _ _). etrans. { apply maponpaths. exact (!(functor_comp R₃ _ _)). } refine (!(functor_comp R₃ _ _) @ _). apply maponpaths. unfold φ. etrans. { rewrite !assoc. apply maponpaths_2. apply (nat_trans_ax (fiber_functor_natural HD₂ HD₃ GG (# F f))). } rewrite !assoc'. etrans. { apply maponpaths. refine (!(functor_comp (fiber_functor GG (F x)) _ _) @ _). apply maponpaths. etrans. { apply maponpaths_2. etrans. { do 2 apply maponpaths. exact (!(functor_comp R₂ _ _)). } apply functor_comp. } rewrite !assoc'. etrans. { apply maponpaths. apply (nat_trans_ax ε₂). } rewrite !assoc. apply maponpaths_2. exact (pr122 P₂ (fiber_functor FF y (R₁ a))). } rewrite id_left. etrans. { apply maponpaths. apply (functor_comp (fiber_functor GG (F x))). } rewrite assoc. refine (!_). etrans. { apply maponpaths_2. exact fiber_functor_natural_comp. } rewrite !assoc'. apply maponpaths. apply maponpaths. cbn. rewrite disp_functor_transportf. rewrite transport_f_f. 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.