Proposition make_h_valued_morphism_laws : partial_setoid_morphism_laws φ. Proof. repeat split ; cbn ; unfold prodtofuntoprod ; cbn ; intros z ; induction z. - use cha_le_glb. intros [ [ [] x ] p ]. use cha_le_glb. intros [ [ [ [] x' ] y ] q ]. cbn in *. use cha_to_le_exp. rewrite cha_lunit_min_top. apply p₁. - use cha_le_glb. intros [ [ [] x ] p ]. use cha_le_glb. intros [ [ [ [] x' ] y ] q ]. cbn in *. use cha_to_le_exp. rewrite cha_lunit_min_top. apply p₂. - use cha_le_glb. intros [ [ [] x₁ ] q₁ ]. use cha_le_glb. intros [ [ [ [] x' ] x₂ ] q₂ ]. cbn in *. use cha_le_glb. intros [ [ [ [ [ ] x₁' ] x₂' ] y₁ ] q₃ ]. cbn in *. use cha_le_glb. intros [ [ [ [ [ [ ] x₁'' ] x₂'' ] y₁' ] y₂ ] q₄ ]. cbn in *. do 3 use cha_to_le_exp. rewrite cha_lunit_min_top. rewrite cha_min_assoc. apply p₃. - use cha_le_glb. intros [ [ [] x ] q₁ ]. use cha_le_glb. intros [ [ [ [] x' ] y₁ ] q₂ ]. use cha_le_glb. intros [ [ [ [ [ ] x'' ] y₁' ] y₂ ] q₃ ]. cbn in *. do 2 use cha_to_le_exp. rewrite cha_lunit_min_top. apply p₄. - use cha_le_glb. intros [ [ [] x ] q ] ; cbn. use cha_to_le_exp. rewrite cha_lunit_min_top. refine (cha_le_trans _ _). { apply p₅. } use cha_lub_le. intros y. use cha_le_lub. + refine (((tt ,, x) ,, y) ,, _). apply idpath. + 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.