Definition make_partial_setoid_morphism (φ : form (X ×h Y)) (Hφ : partial_setoid_morphism_laws φ) : partial_setoid_morphism := φ ,, Hφ. Coercion partial_setoid_morphism_to_form (φ : partial_setoid_morphism) : form (X ×h Y). Proof. exact (pr1 φ). 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.