Proposition per_subobject_forall_laws : per_subobject_laws per_subobject_forall_form. Proof. split. - use forall_intro. use impl_intro. use weaken_right. unfold per_subobject_forall_form. pose (b := π₂ (tm_var (𝟙 ×h B))). fold b. simplify_form. rewrite partial_setoid_subst. use weaken_left. simplify. apply hyperdoctrine_hyp. - do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use to_per_subobject_forall_form. + use weaken_left. exact (partial_setoid_refl_r (hyperdoctrine_hyp _)). + use forall_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 impl_intro. use per_subobject_forall_form_all. * exact b₁. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * 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. 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.