Proposition inv_of_comm_nat_z_iso (xx : D[{x}]) : nat_z_iso_inv (comm_nat_z_iso HD f g h k p) (right_adjoint P₁ xx) = τ (R₁ xx). Proof. unfold τ. cbn -[fiber_functor_from_cleaving_comp_nat_z_iso fiber_functor_on_eq_nat_z_iso]. rewrite !assoc'. apply maponpaths. apply maponpaths_2. refine (!(id_right _) @ _). use z_iso_inv_on_right. cbn. refine (_ @ pr1_idtoiso_concat _ _). refine (!_). etrans. { do 2 apply maponpaths. refine (!(maponpathscomp0 (λ q, pr1 (HD w z q (R₁ xx))) _ _) @ _). rewrite pathsinv0r. apply idpath. } apply idpath. 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.