Proposition hyperdoctrine_proof_subst {H : preorder_hyperdoctrine} {Γ₁ Γ₂ : ty H} {Δ φ : form Γ₂} (s : tm Γ₁ Γ₂) (p : Δ ⊢ φ) : Δ [ s ] ⊢ φ [ s ]. Proof. exact (#(fiber_functor_from_cleaving _ (hyperdoctrine_cleaving H) s) p). 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.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Preservation.