Proposition per_subobject_exists_subst : per_subobject_mor_law (id_partial_setoid_morphism A₃) (per_subobject_subst s₂ (per_subobject_exists s₁ φ)) (per_subobject_exists s₃ (per_subobject_subst s₄ φ)). Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn ; unfold per_subobject_exists_form ; cbn. simplify_form. rewrite partial_setoid_subst. simplify. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite !conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. use hyp_rtrans. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite !conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. pose (h := per_subobject_exists_subst_pb_fun). simple refine (exists_elim (partial_setoid_mor_hom_exists h _) _). - apply tm_var. - cbn. use eq_in_formula_to_partial_setoid. + apply hyperdoctrine_refl. + simplify. pose (Γ := (((𝟙 ×h A₃) ×h A₃) ×h A₁) ×h A₂). fold Γ. pose (a₃ := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (a₃' := π₂ (π₁ (π₁ (tm_var Γ)))). pose (a₁ := π₂ (π₁ (tm_var Γ))). pose (a₂ := π₂ (tm_var Γ)). fold a₁ a₂ a₃ a₃'. apply hyperdoctrine_hyp. - simplify_form. rewrite !partial_setoid_subst. simplify. pose (Γ := ((((𝟙 ×h A₃) ×h A₃) ×h A₁) ×h A₂) ×h A₄). fold Γ. pose (a₃ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))). pose (a₃' := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (a₁ := π₂ (π₁ (π₁ (tm_var Γ)))). pose (a₂ := π₂ (π₁ (tm_var Γ))). pose (a₄ := π₂ (tm_var Γ)). fold a₁ a₂ a₃ a₃' a₄. use exists_intro. { exact a₄. } simplify. fold a₃'. use conj_intro. + use partial_setoid_mor_eq_defined. * exact a₄. * exact a₃. * use weaken_right. exact (partial_setoid_mor_cod_defined h _ _ (hyperdoctrine_hyp _)). * do 3 use weaken_left. apply hyperdoctrine_hyp. * use per_subobject_exists_subst_pb_fun_proj2. ** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. simplify_form. rewrite partial_setoid_subst. simplify. apply hyperdoctrine_hyp. + use exists_intro. { exact a₂. } simplify. use conj_intro. * use per_subobject_exists_subst_pb_fun_proj1. ** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_left. simplify_form. rewrite partial_setoid_subst. simplify. apply hyperdoctrine_hyp. * use weaken_left. 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.