Proposition per_subobject_false_subst {Γ₁ Γ₂ : partial_setoid H} (s : partial_setoid_morphism Γ₁ Γ₂) : per_subobject_mor_law (id_partial_setoid_morphism Γ₁) (per_subobject_subst s (per_subobject_false Γ₂)) (per_subobject_false Γ₁). Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. use hyp_sym. rewrite !exists_subst. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite !conj_subst. use hyp_ltrans. use weaken_right. do 2 use weaken_right. simplify. 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.FiberwiseInitial. 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.Logic.SubobjectDispCat.