Definition partial_setoid_mono_eq {H : first_order_hyperdoctrine} {X Y : partial_setoid H} (φ : partial_setoid_morphism X Y) (Hφ : isMonic (C := category_of_partial_setoids H) φ) {Γ : ty H} {Δ : form Γ} {x₁ x₂ : tm Γ X} {y : tm Γ Y} (p₁ : Δ ⊢ φ[⟨ x₁ , y ⟩]) (p₂ : Δ ⊢ φ[⟨ x₂ , y ⟩]) : Δ ⊢ x₁ ~ x₂.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain. Require Import UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects.