Definition cod_fiber_has_dependent_sum {C : category} (HC : Pullbacks C) (HD := disp_codomain_cleaving HC) : has_dependent_sums HD. Proof. simple refine (_ ,, _). - exact (λ x y f, is_right_adjoint_cod_fiber_functor HC f). - exact (λ w x y z f g h k p H, cod_left_beck_chevalley HC f g h k p H). 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.