Proposition isaprop_partial_setoid_morphism_laws (φ : form (X ×h Y)) : isaprop (partial_setoid_morphism_laws φ). Proof. repeat (use isapropdirprod) ; apply invproofirrelevance ; intros ? ? ; apply hyperdoctrine_proof_eq. Qed.
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.