Proposition per_subobject_forall_form_all {Γ : ty H} {Δ : form Γ} {a : tm Γ A} {b : tm Γ B} (p : Δ ⊢ per_subobject_forall_form [ b ]) (q : Δ ⊢ φ [ ⟨ a , b ⟩ ]) : Δ ⊢ ψ [ a ]. Proof. use (impl_elim q). refine (hyperdoctrine_cut p _). unfold per_subobject_forall_form. simplify_form. use weaken_right. simplify. refine (hyperdoctrine_cut _ _). { exact (forall_elim (hyperdoctrine_hyp _) a). } simplify. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DualBeckChevalley. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Existential.