Definition partial_setoid_mor_hom_exists_law (φ : form (X ×h Y)) : UU := let x := π₂ (tm_var _) : tm (𝟙 ×h X) X in let y := π₂ (tm_var _) : tm ((𝟙 ×h X) ×h Y) Y in ⊤ ⊢ (∀h (x ~ x ⇒ ∃h (φ [ ⟨ x [ π₁ (tm_var _) ]tm , y ⟩ ]))).
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.