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