Definition dependent_sums_per_subobject : has_dependent_sums (disp_cat_per_subobject_cleaving H). Proof. use make_has_dependent_sums_poset. - apply locally_prop_disp_cat_per_subobject. - intros A B φ ψ. exact (per_subobject_exists φ ψ). - intros A B φ ψ. exact (per_subobject_exists_intro φ ψ). - intros A B φ ψ χ p. exact (per_subobject_exists_elim φ ψ p). - intros A₁ A₂ A₃ A₄ s₁ s₂ s₃ s₄ p Hp φ. exact (per_subobject_exists_subst p Hp φ). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.