Proposition morphism_to_equalizer_partial_setoid_eq : partial_setoid_comp_morphism morphism_to_equalizer_partial_setoid equalizer_partial_setoid_morphism = χ. Proof. use eq_partial_setoid_morphism ; cbn. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. 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 (partial_setoid_mor_eq_defined χ). + exact w. + exact x₂. + use weaken_left. exact (partial_setoid_mor_dom_defined χ _ _ (hyperdoctrine_hyp _)). + use weaken_right. use (from_eq_in_equalizer_partial_setoid x₂ x₁). apply hyperdoctrine_hyp. + use weaken_left. apply hyperdoctrine_hyp. - use exists_intro. + exact (π₂ (tm_var _)). + simplify_form. rewrite partial_setoid_subst. simplify. rewrite <- hyperdoctrine_pair_eta. simplify. pose (w := π₁ (tm_var (W ×h X))). pose (x := π₂ (tm_var (W ×h X))). fold w x. use conj_intro. * apply hyperdoctrine_hyp. * use eq_in_equalizer_partial_setoid. ** use (partial_setoid_mor_cod_defined χ w x). unfold w, x. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. ** rewrite <- (hyperdoctrine_id_subst χ). rewrite (hyperdoctrine_pair_eta (tm_var (W ×h X))). apply morphism_to_equalizer_partial_setoid_laws_eq. 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.