Proposition morphism_to_equalizer_partial_setoid_unique : ζ = morphism_to_equalizer_partial_setoid. Proof. use eq_partial_setoid_morphism ; cbn. - use (from_eq_partial_setoid_morphism_f q) ; cbn. simplify_form. rewrite partial_setoid_subst. use exists_intro. + exact (π₂ (tm_var _)). + simplify_form. rewrite partial_setoid_subst. simplify. rewrite <- hyperdoctrine_pair_eta. simplify_form. pose (w := π₁ (tm_var (W ×h X))). pose (x := π₂ (tm_var (W ×h X))). cbn. fold w x. use conj_intro. * apply hyperdoctrine_hyp. * use (partial_setoid_mor_cod_defined ζ w x). unfold w, x. rewrite <- hyperdoctrine_pair_eta. simplify_form. apply hyperdoctrine_hyp. - pose (w := π₁ (tm_var (W ×h X))). pose (x := π₂ (tm_var (W ×h X))). fold w x. pose (from_eq_partial_setoid_morphism_b q (hyperdoctrine_hyp (χ [ ⟨ w , x ⟩ ]))) as r. cbn in r. rewrite exists_subst in r. use (exists_elim r). unfold w, x ; clear r w x. simplify_form. rewrite partial_setoid_subst. simplify. pose (w := π₁ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₁ := π₂ (π₁ (tm_var ((W ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((W ×h X) ×h X))). fold w x₁ x₂. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((W ×h X) ×h X)))). fold w x₁. use weaken_right. use (partial_setoid_mor_eq_defined ζ). + exact w. + exact x₂. + use weaken_left. use (partial_setoid_mor_dom_defined ζ w x₂). apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. apply hyperdoctrine_hyp. Qed.
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.