Proposition per_subobject_truth_subst {Γ₁ Γ₂ : partial_setoid H} (s : partial_setoid_morphism Γ₁ Γ₂) : per_subobject_mor_law (id_partial_setoid_morphism Γ₁) (per_subobject_truth Γ₁) (per_subobject_subst s (per_subobject_truth Γ₂)). Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. rewrite !partial_setoid_subst. simplify. pose (γ₁ := π₂ (π₁ (tm_var ((𝟙 ×h Γ₁) ×h Γ₁)))). pose (γ₂ := π₂ (tm_var ((𝟙 ×h Γ₁) ×h Γ₁))). fold γ₁ γ₂. simple refine (exists_elim (partial_setoid_mor_hom_exists s _) _). - exact γ₂. - use weaken_left. use partial_setoid_refl_r. { exact γ₁. } apply hyperdoctrine_hyp. - unfold γ₁, γ₂ ; clear γ₁ γ₂. pose (γ₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))))). pose (γ₂ := π₂ (π₁ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂)))). pose (γ₃ := π₂ (tm_var (((𝟙 ×h Γ₁) ×h Γ₁) ×h Γ₂))). rewrite exists_subst. use exists_intro. { exact γ₃. } rewrite partial_setoid_subst. simplify_form. rewrite !partial_setoid_subst. simplify. fold γ₁ γ₂ γ₃. use conj_intro. + use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. use (partial_setoid_mor_cod_defined s). * exact γ₂. * 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.FiberwiseTerminal. 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.