Definition has_dependent_products_h_valued_sets : has_dependent_products cleaving_h_valued_sets. Proof. use make_has_dependent_products_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_glb_le ; [ exact (x ,, idpath _) | ] ; cbn ; apply cha_le_refl). - abstract (intros X Y f P Q p y ; cbn in * ; use cha_le_glb ; 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_le_glb ; intros z ; induction z as [ z zp ] ; use cha_glb_le ; [ 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.