Definition equalizers_partial_setoid (H : first_order_hyperdoctrine) : Equalizers (category_of_partial_setoids H). Proof. intros X Y φ ψ. use make_Equalizer. - exact (equalizer_partial_setoid φ ψ). - exact (equalizer_partial_setoid_morphism φ ψ). - exact (equalizer_partial_setoid_morphism_eq φ ψ). - intros W χ p. use make_iscontr. + simple refine (_ ,, _) ; cbn. * exact (morphism_to_equalizer_partial_setoid φ ψ χ p). * exact (morphism_to_equalizer_partial_setoid_eq φ ψ χ p). + abstract (intros ζ ; use subtypePath ; [ intro ; apply homset_property | ] ; cbn ; apply morphism_to_equalizer_partial_setoid_unique ; exact (pr2 ζ)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Equalizers. 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.