Definition cod_left_beck_chevalley : left_beck_chevalley HD f g h k p (is_right_adjoint_cod_fiber_functor HC f) (is_right_adjoint_cod_fiber_functor HC h). Proof. intro φ. use is_z_iso_fiber_from_is_z_iso_disp. use is_z_iso_disp_codomain. use is_z_isomorphism_path. - exact (cod_left_beck_chevalley_mor φ). - exact (cod_left_beck_chevalley_eq φ). - exact (is_z_isomorphism_cod_left_beck_chevalley_mor φ). Defined.
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.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.