Proposition per_subobject_forall_intro : per_subobject_mor_law (id_partial_setoid_morphism B) χ per_subobject_forall. Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. rewrite partial_setoid_subst. simplify. use to_per_subobject_forall_form. - pose (b₁ := π₂ (π₁ (tm_var ((𝟙 ×h B) ×h B)))). pose (b₂ := π₂ (tm_var ((𝟙 ×h B) ×h B))). fold b₁ b₂. use weaken_left. exact (partial_setoid_refl_r (hyperdoctrine_hyp _)). - use forall_intro. use impl_intro. simplify_form. rewrite partial_setoid_subst. simplify. pose (b₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h B) ×h B) ×h A))))). pose (b₂ := π₂ (π₁ (tm_var (((𝟙 ×h B) ×h B) ×h A)))). pose (a := π₂ (tm_var (((𝟙 ×h B) ×h B) ×h A))). fold a b₁ b₂. use (per_subobject_mor p). + exact a. + cbn. rewrite partial_setoid_subst. simplify. use weaken_right. use (partial_setoid_mor_dom_defined φ a b₂). apply hyperdoctrine_hyp. + cbn. simplify. use exists_intro. { exact b₁. } simplify. use conj_intro. * use (partial_setoid_mor_eq_defined φ). ** exact a. ** exact b₂. ** use weaken_right. use (partial_setoid_mor_dom_defined φ a b₂). apply hyperdoctrine_hyp. ** use partial_setoid_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. 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.