Proposition per_subobject_exists_intro : per_subobject_mor_law (id_partial_setoid_morphism A) ψ (per_subobject_subst φ per_subobject_exists). Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn ; unfold per_subobject_exists_form. simplify_form. rewrite partial_setoid_subst. simplify. simple refine (exists_elim (partial_setoid_mor_hom_exists φ _) _). - exact (π₂ (π₁ (tm_var ((𝟙 ×h A) ×h A)))). - use weaken_left. exact (partial_setoid_refl_l (hyperdoctrine_hyp _)). - simplify_form. rewrite !partial_setoid_subst. simplify. pose (a₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h B))))). pose (a₂ := π₂ (π₁ (tm_var (((𝟙 ×h A) ×h A) ×h B)))). pose (b := π₂ (tm_var (((𝟙 ×h A) ×h A) ×h B))). fold a₁ a₂ b. use exists_intro. { exact b. } simplify. fold a₂. use conj_intro. + use (partial_setoid_mor_eq_defined φ). ** exact a₁. ** exact b. ** do 2 use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. exact (partial_setoid_mor_cod_defined φ a₁ b (hyperdoctrine_hyp _)). ** use weaken_right. apply hyperdoctrine_hyp. + use exists_intro. { exact a₁. } simplify. use conj_intro. * 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. 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.PERTerminal. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat.