Definition per_of_h_valued_set {X : h_valued_set} (x y : X) : H := pr12 X (x ,, y).
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.