Proposition equalizer_partial_setoid_morphism_eq : partial_setoid_comp_morphism equalizer_partial_setoid_morphism φ = partial_setoid_comp_morphism 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. use (exists_elim (from_eq_in_equalizer_partial_setoid_ex _ _ (weaken_left (hyperdoctrine_hyp _) _))). simplify_form. rewrite !partial_setoid_subst. simplify. use exists_intro. + exact (π₂ (π₁ (tm_var _))). + simplify_form. rewrite partial_setoid_subst. simplify. cbn. pose (x₁ := π₁ (π₁ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y))))). pose (y₁ := π₂ (π₁ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y))))). pose (x₂ := π₂ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y)))). pose (y₂ := π₂ (tm_var (((X ×h Y) ×h X) ×h Y))). fold x₁ y₁ x₂ y₂. use conj_intro. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use (partial_setoid_mor_eq_defined ψ). ** exact x₁. ** exact y₂. ** do 2 use weaken_left. use (from_eq_in_equalizer_partial_setoid x₁ x₂). apply hyperdoctrine_hyp. ** use (partial_setoid_mor_unique_im φ). *** exact x₁. *** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. *** use weaken_left. use (partial_setoid_mor_eq_defined φ). **** exact x₂. **** exact y₁. **** use partial_setoid_sym. use weaken_left. use (from_eq_in_equalizer_partial_setoid x₁ x₂). apply hyperdoctrine_hyp. **** use weaken_right. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). **** use weaken_right. apply hyperdoctrine_hyp. ** do 2 use weaken_right. apply hyperdoctrine_hyp. - use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. use (exists_elim (from_eq_in_equalizer_partial_setoid_ex _ _ (weaken_left (hyperdoctrine_hyp _) _))). simplify_form. rewrite !partial_setoid_subst. simplify. use exists_intro. + exact (π₂ (π₁ (tm_var _))). + simplify_form. rewrite partial_setoid_subst. simplify. cbn. pose (x₁ := π₁ (π₁ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y))))). pose (y₁ := π₂ (π₁ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y))))). pose (x₂ := π₂ (π₁ (tm_var (((X ×h Y) ×h X) ×h Y)))). pose (y₂ := π₂ (tm_var (((X ×h Y) ×h X) ×h Y))). fold x₁ y₁ x₂ y₂. use conj_intro. * do 2 use weaken_left. apply hyperdoctrine_hyp. * use (partial_setoid_mor_eq_defined φ). ** exact x₁. ** exact y₂. ** do 2 use weaken_left. use (from_eq_in_equalizer_partial_setoid x₁ x₂). apply hyperdoctrine_hyp. ** use (partial_setoid_mor_unique_im ψ). *** exact x₂. *** use (partial_setoid_mor_eq_defined ψ). **** exact x₁. **** exact y₂. **** do 2 use weaken_left. use (from_eq_in_equalizer_partial_setoid x₁ x₂). apply hyperdoctrine_hyp. **** do 2 use weaken_right. exact (partial_setoid_mor_cod_defined ψ _ _ (hyperdoctrine_hyp _)). **** do 2 use weaken_right. apply hyperdoctrine_hyp. *** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. ** use weaken_right. 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.