Proposition mor_to_tripos_power_f {H : tripos} (X : ty H) (Γ : ty H) (R : form (X ×h Γ)) (Δ : form (X ×h Γ)) (x := π₁ (tm_var (X ×h Γ))) (γ := π₂ (tm_var (X ×h Γ))) (p : Δ ⊢ R) : Δ ⊢ x ∈ ({{ R }} [ γ ]tm). Proof. refine (hyperdoctrine_cut p _). exact (hyperdoctrine_formula_eq_f (mor_to_tripos_power_eq X Γ R)). Qed.
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.