Proposition morphism_to_equalizer_partial_setoid_laws : partial_setoid_morphism_laws morphism_to_equalizer_partial_setoid_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h X)))). pose (x := π₂ (tm_var ((𝟙 ×h W) ×h X))). fold w x. use (partial_setoid_mor_dom_defined χ w x). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law ; cbn. do 2 use forall_intro. use impl_intro. use weaken_right. simplify. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h X)))). pose (x := π₂ (tm_var ((𝟙 ×h W) ×h X))). fold w x. use eq_in_equalizer_partial_setoid. + use (partial_setoid_mor_cod_defined χ w x). apply hyperdoctrine_hyp. + apply morphism_to_equalizer_partial_setoid_laws_eq. - unfold partial_setoid_mor_eq_defined_law ; cbn. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. simplify. pose (w₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h W) ×h W) ×h X) ×h X)))))). pose (w₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h W) ×h W) ×h X) ×h X))))). pose (x₁ := π₂ (π₁ (tm_var ((((𝟙 ×h W) ×h W) ×h X) ×h X)))). pose (x₂ := π₂ (tm_var ((((𝟙 ×h W) ×h W) ×h X) ×h X))). fold w₁ w₂ x₁ x₂. use (partial_setoid_mor_eq_defined χ). + exact w₁. + exact x₁. + do 2 use weaken_left. apply hyperdoctrine_hyp. + use (from_eq_in_equalizer_partial_setoid x₁ x₂). use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law ; cbn. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify. pose (w := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h X))))). pose (x₁ := π₂ (π₁ (tm_var (((𝟙 ×h W) ×h X) ×h X)))). pose (x₂ := π₂ (tm_var (((𝟙 ×h W) ×h X) ×h X))). fold w x₁ x₂. use eq_in_equalizer_partial_setoid. + use (partial_setoid_mor_unique_im χ). * exact w. * use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. apply morphism_to_equalizer_partial_setoid_laws_eq. - unfold partial_setoid_mor_hom_exists_law ; cbn. use forall_intro. use impl_intro. use weaken_right. use (exists_elim (partial_setoid_mor_hom_exists χ (hyperdoctrine_hyp _))). simplify_form. use exists_intro. + exact (π₂ (tm_var _)). + simplify_form. rewrite partial_setoid_subst. simplify. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h X)))). pose (x := π₂ (tm_var ((𝟙 ×h W) ×h X))). fold w x. use weaken_right. 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.