Proposition per_subobject_subst_mor : per_subobject_mor_law φ per_subobject_subst ψ. Proof. do 2 use forall_intro. use impl_intro. use weaken_right. use impl_intro. cbn. unfold ζ. use hyp_sym. rewrite !exists_subst. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite !conj_subst. use hyp_ltrans. use weaken_right. simplify. pose (x₁ := π₂ (π₁ (tm_var (((𝟙 ×h Y) ×h X) ×h X)))). pose (x₂ := π₂ (tm_var (((𝟙 ×h Y) ×h X) ×h X))). pose (y := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Y) ×h X) ×h X))))). fold x₁ x₂ y. use (per_subobject_eq ψ). - exact x₂. - use (partial_setoid_mor_unique_im φ). + exact y. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. + 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.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. 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.