Definition tripos_generic_predicate (H : tripos) : generic_predicate H. Proof. use make_generic_predicate. - exact (ℙ 𝟙). - exact (let P := tm_var (ℙ 𝟙) in !! ∈ P). - intros Γ A. simple refine (_ ,, _). + exact {{ A [ π₂ (tm_var _) ] }}. + abstract (cbn ; rewrite tripos_in_subst ; simplify ; pose (maponpaths (λ φ, φ [ ⟨ !! , tm_var _ ⟩ ]) (mor_to_tripos_power_eq 𝟙 Γ (A [ π₂ (tm_var _) ]))) as p ; cbn in p ; rewrite !hyperdoctrine_comp_subst in p ; rewrite hyperdoctrine_pr2_subst in p ; rewrite var_tm_subst in p ; rewrite hyperdoctrine_pair_pr2 in p ; rewrite hyperdoctrine_id_subst in p ; refine (p @ _) ; clear p ; use hyperdoctrine_formula_eq ; simplify ; apply hyperdoctrine_hyp). 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.