Proposition trans_per_of_h_valued_set {X : h_valued_set} (x y z : X) : ((x ~_{X} y ∧ y ~_{X} z) ≤ (x ~_{X} z))%heyting. Proof. pose (pr222 X tt) as p. cbn in p ; unfold prodtofuntoprod in p ; cbn in p. assert (⊤ ≤ (x ~_{X} y ⇒ y ~_{X} z ⇒ x ~_{X} z))%heyting as q. { refine (cha_le_trans p _). simple refine (cha_le_trans (cha_glb_le_pt _ _) _). { refine ((tt ,, x) ,, _). apply idpath. } cbn. simple refine (cha_le_trans (cha_glb_le_pt _ _) _). { refine (((tt ,, x) ,, y) ,, _). apply idpath. } cbn. simple refine (cha_le_trans (cha_glb_le_pt _ _) _). { refine ((((tt ,, x) ,, y) ,, z) ,, _). cbn. apply idpath. } cbn. apply cha_le_refl. } pose proof (cha_from_le_exp q) as r. rewrite cha_lunit_min_top in r. exact (cha_from_le_exp 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.