Lemma dual_left_beck_chevalley_nat_trans_ob_alt (xx : D[{x}]) : ℓ (G(R₁ xx)) · #F(ψ₁ _) · ε₁ xx = # L₂ (τ (R₁ xx)) · (ψ₂ (F (R₁ xx)) · ε₁ xx). Proof. rewrite dual_left_beck_chevalley_nat_trans_ob. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. etrans. { do 2 apply maponpaths. refine (!_). apply (nat_trans_ax ψ₂ _ _ (# F (ψ₁ (R₁ xx)))). } rewrite !assoc. apply maponpaths_2. rewrite <- !functor_comp. refine (!(functor_comp _ _ _) @ _). apply maponpaths. rewrite !assoc'. etrans. { apply maponpaths. refine (!_). apply (nat_trans_ax τ). } refine (_ @ id_left _). rewrite !assoc. apply maponpaths_2. refine (!(functor_comp _ _ _) @ _ @ functor_id _ _). apply maponpaths. apply (pr222 S₁). 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.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.