Proposition per_subobject_exists_elim : per_subobject_mor_law (id_partial_setoid_morphism B) per_subobject_exists χ. Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. cbn ; unfold per_subobject_exists_form. simplify_form. rewrite partial_setoid_subst. simplify. use hyp_sym. simple refine (exists_elim (weaken_left (hyperdoctrine_hyp _) _) _). rewrite conj_subst. use hyp_ltrans. use weaken_right. 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₂. pose (Δ := b₁ ~ b₂ ∧ φ [⟨ a, b₁ ⟩] ∧ ψ [a]). assert (Δ ⊢ (id_partial_setoid_morphism A) [⟨ a , a ⟩]) as r₁. { cbn. rewrite partial_setoid_subst. simplify. unfold Δ. use weaken_right. use weaken_left. use (partial_setoid_mor_dom_defined φ a b₁). apply hyperdoctrine_hyp. } assert (Δ ⊢ ψ [a]) as r₂. { unfold Δ. do 2 use weaken_right. apply hyperdoctrine_hyp. } pose (per_subobject_mor p r₁ r₂) as r₃. unfold per_subobject_subst in r₃. cbn in r₃. rewrite exists_subst in r₃. refine (exists_elim r₃ _). unfold Δ ; clear Δ r₁ r₂ r₃. unfold a, b₁, b₂ ; clear a b₁ b₂. simplify_form. rewrite partial_setoid_subst. simplify. pose (b₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h B) ×h B) ×h A) ×h B)))))). pose (b₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h B) ×h B) ×h A) ×h B))))). pose (a := π₂ (π₁ (tm_var ((((𝟙 ×h B) ×h B) ×h A) ×h B)))). pose (b₃ := π₂ (tm_var ((((𝟙 ×h B) ×h B) ×h A) ×h B))). fold a b₁ b₂ b₃. use per_subobject_eq. - exact b₃. - use partial_setoid_trans. + exact b₁. + use (partial_setoid_mor_unique_im φ). * exact a. * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + do 2 use weaken_left. apply hyperdoctrine_hyp. - do 2 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.