Lemma dual_right_beck_chevalley_nat_trans_ob (xx : D[{x}]) : ρ xx = η₂(G(R₁ xx)) · #R₂(τ(R₁ xx)) · #R₂(#K(ε₁ xx)). Proof. unfold ρ. etrans. { apply right_beck_chevalley_nat_trans_ob. } apply maponpaths_2. do 2 apply maponpaths. apply inv_of_comm_nat_z_iso. 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.