Definition precategory_ob_mor_of_partial_setoids : precategory_ob_mor. Proof. use make_precategory_ob_mor. - exact (partial_setoid H). - exact (λ (X Y : partial_setoid H), partial_setoid_morphism X Y). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.