Definition has_dependent_sums_h_valued_sets : has_dependent_sums cleaving_h_valued_sets. Proof. use make_has_dependent_sums_poset. - exact locally_propositional_h_valued_sets. - exact (λ (X Y : hSet) (f : X → Y) (P : X → H) (y : Y), \/_{ z : ∑ (x : X), f x = y } P (pr1 z)). - abstract (intros X Y f P x ; cbn in * ; use cha_le_lub ; [ exact (x ,, idpath _) | ] ; cbn ; apply cha_le_refl). - abstract (intros X Y f P Q p y ; cbn in * ; use cha_lub_le ; intros z ; induction z as [ x q ] ; induction q ; cbn ; apply p). - abstract (intros Y₂ Y₁ X₂ X₁ f₁ f₂ g₁ g₂ p Hp P y ; cbn in * ; use cha_lub_le ; intros z ; induction z as [ z zp ] ; use cha_le_lub ; [ exact (el_pullback_set Hp z y zp ,, el_pullback_set_pr2 Hp z y zp) | ] ; cbn ; rewrite el_pullback_set_pr1 ; apply cha_le_refl). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.