Proposition h_valued_morphism_eq_defined (x₁ x₂ : X) (y₁ y₂ : Y) : ((x₁ ~_{X} x₂ ∧ y₁ ~_{Y} y₂ ∧ f x₁ y₁) ≤ f x₂ y₂)%heyting. Proof. refine (@partial_setoid_mor_eq_defined _ _ _ f unitset (λ _, (x₁ ~_{X} x₂ ∧ y₁ ~_{Y} y₂ ∧ f x₁ y₁)%heyting) (λ _, x₁) (λ _, x₂) (λ _, y₁) (λ _, y₂) _ _ _ tt) ; cbn ; unfold prodtofuntoprod ; cbn ; intro. - apply cha_min_le_l. - refine (cha_le_trans _ _). { apply cha_min_le_r. } apply cha_min_le_l. - refine (cha_le_trans _ _). { apply cha_min_le_r. } apply cha_min_le_r. 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.