Definition make_h_valued_set (X : hSet) (R : X → X → H) (sym : ∏ (x y : X), R x y = R y x) (trans : ∏ (x y z : X), ((R x y ∧ R y z) ≤ R x z)%heyting) : h_valued_set. Proof. use make_partial_setoid. - exact X. - use make_per. + exact (λ x, R (pr1 x) (pr2 x)). + repeat split ; intros [] ; cbn. * abstract (use cha_le_glb ; intros i ; induction i as [ [ [] x ] p ] ; use cha_le_glb ; intros i ; induction i as [ [ [ [] y ] z ] q ] ; cbn in * ; use cha_to_le_exp ; rewrite cha_lunit_min_top ; rewrite sym ; apply cha_le_refl). * abstract (use cha_le_glb ; intros i ; induction i as [ [ [] x₁ ] p ] ; use cha_le_glb ; intros i ; induction i as [ [ [ [] x₂ ] x₃ ] q ] ; use cha_le_glb ; intros i ; induction i as [ [ [ [ [] x₄ ] x₅ ] x₆ ] r ] ; cbn in * ; do 2 use cha_to_le_exp ; rewrite cha_lunit_min_top ; apply trans). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.ElementaryTopos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.HValuedPredicates. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. Require Import UniMath.CategoryTheory.Hyperdoctrines.TriposToTopos.