Definition partial_setoid_morphism_laws (φ : form (X ×h Y)) : UU := partial_setoid_mor_dom_defined_law φ × partial_setoid_mor_cod_defined_law φ × partial_setoid_mor_eq_defined_law φ × partial_setoid_mor_unique_im_law φ × partial_setoid_mor_hom_exists_law φ.
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.