Definition mono_codomain_has_dependent_sums : has_dependent_sums HD. Proof. use make_has_dependent_sums_poset. - apply locally_propositional_mono_cod_disp_cat. - exact (λ y₁ y₂ f xg, mono_codomain_exists f xg). - exact (λ y₁ y₂ f xg, mono_codomain_exists_intro f xg). - intros. apply mono_codomain_exists_elim. exact p. - intros x₁ x₂ x₃ x₄ s₁ s₂ s₃ s₄ p Hp yg. exact (mono_codomain_exists_stable Hp yg). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts.