Proposition h_valued_morphism_hom_exists (x : X) : (x ~_{X} x ≤ \/_{ y } f x y)%heyting. Proof. refine (cha_le_trans _ _). { refine (@partial_setoid_mor_hom_exists _ _ _ f unitset (λ _, x ~_{X} x)%heyting (λ _, x) _ tt). cbn ; unfold prodtofuntoprod ; cbn ; intro. apply cha_le_refl. } cbn ; unfold prodtofuntoprod ; cbn. use cha_lub_le ; cbn. intro i. induction i as [ [ [] y ] p ] ; cbn. use cha_le_lub. { exact y. } apply cha_le_refl. Qed.
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.