Definition make_generic_predicate {H : first_order_hyperdoctrine} (Ω : ty H) (prf : form Ω) (HΩ : is_generic_predicate Ω prf) : generic_predicate H := Ω ,, prf ,, HΩ. Coercion ty_of_generic_predicate {H : first_order_hyperdoctrine} (Ω : generic_predicate H) : ty H. Proof. exact (pr1 Ω). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.