Proposition disp_cat_id_comp_per_subobject : disp_cat_id_comp (category_of_partial_setoids H) disp_cat_ob_mor_per_subobject. Proof. split. - cbn. intros X ψ. do 2 use forall_intro. use impl_intro. use weaken_right. pose (x₁ := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((𝟙 ×h X) ×h X))). fold x₁ x₂. rewrite partial_setoid_subst. simplify. use impl_intro. use per_subobject_eq. + exact x₁. + use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - intros X Y Z φ₁ φ₂ ψ₁ ψ₂ ψ₃ p q. cbn -[per_subobject_mor_law] in * ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. rewrite exists_subst. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite impl_subst. pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h Z) ×h Y))))). pose (z := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h Z) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h X) ×h Z) ×h Y))). simplify. fold x y z. use impl_intro. use (per_subobject_mor q). + exact y. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use (per_subobject_mor p). * exact x. * do 2 use weaken_left. apply hyperdoctrine_hyp. * 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.