Lemma dual_left_beck_chevalley_nat_trans_ob_alt' (xx : D[{x}]) : #H(φ₁(R₂(K xx))) · τ(L₁(R₂(K xx))) = φ₂ _ · #K(ℓ(R₂(K xx))). Proof. rewrite dual_left_beck_chevalley_nat_trans_ob'. refine (!_). rewrite !functor_comp. rewrite !assoc. etrans. { do 2 apply maponpaths_2. refine (!_). apply (nat_trans_ax φ₂). } cbn. rewrite !assoc'. apply maponpaths. rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply (nat_trans_ax φ₂). } cbn. refine (_ @ id_right _). rewrite !assoc'. 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.