Definition disp_cat_ob_mor_per_subobject : disp_cat_ob_mor (category_of_partial_setoids H). Proof. simple refine (_ ,, _). - exact (λ (X : partial_setoid H), per_subobject X). - exact (λ (X Y : partial_setoid H) (ψ₁ : per_subobject X) (ψ₂ : per_subobject Y) (φ : partial_setoid_morphism X Y), per_subobject_mor_law φ ψ₁ ψ₂). Defined.
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.