Proposition eq_partial_setoid_morphism {φ₁ φ₂ : partial_setoid_morphism} (p : φ₁ ⊢ φ₂) (q : φ₂ ⊢ φ₁) : φ₁ = φ₂. Proof. use subtypePath. { intro. apply isaprop_partial_setoid_morphism_laws. } use hyperdoctrine_formula_eq. - exact p. - exact q. 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.