Definition disp_cat_ob_mor_h_valued_sets : disp_cat_ob_mor SET. Proof. simple refine (_ ,, _). - exact (λ (X : hSet), X → H). - exact (λ (X Y : hSet) (P : X → H) (Q : Y → H) (f : X → Y), ∏ (x : X), P x ≤ Q(f x)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.