Proposition equalizer_partial_setoid_morphism_laws : partial_setoid_morphism_laws equalizer_partial_setoid_morphism_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law. pose (T := equalizer_partial_setoid). pose (T' := X). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. unfold equalizer_partial_setoid_morphism_form. fold x y. cbn. rewrite partial_setoid_subst. simplify. use forall_intro. use forall_intro. use impl_intro. use weaken_right. exact (partial_setoid_refl_l (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_cod_defined_law. pose (T := equalizer_partial_setoid). pose (T' := X). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. unfold equalizer_partial_setoid_morphism_form. fold x y. cbn. rewrite partial_setoid_subst. simplify. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use partial_setoid_refl_r. + exact x. + use from_eq_in_equalizer_partial_setoid. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law. pose (T := equalizer_partial_setoid). pose (T' := X). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T')))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T'))))). pose (y₁ := π₂ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T')))). pose (y₂ := π₂ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T'))). unfold T, T' in *. unfold equalizer_partial_setoid_morphism_form. fold x₁ x₂ y₁ y₂. cbn. rewrite !partial_setoid_subst. simplify. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use partial_setoid_trans. + exact x₁. + use partial_setoid_sym. do 2 use weaken_left. apply hyperdoctrine_hyp. + use partial_setoid_trans. * exact y₁. * use weaken_right. apply hyperdoctrine_hyp. * use hyp_ltrans. use weaken_right. use eq_in_equalizer_partial_setoid. ** use weaken_left. apply hyperdoctrine_hyp. ** use weaken_right. use from_eq_in_equalizer_partial_setoid_ex. *** exact x₁. *** use partial_setoid_sym. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. pose (T := equalizer_partial_setoid). pose (T' := X). pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h T) ×h T') ×h T'))))). pose (y₁ := π₂ (π₁ (tm_var (((𝟙 ×h T) ×h T') ×h T')))). pose (y₂ := π₂ (tm_var (((𝟙 ×h T) ×h T') ×h T'))). unfold T, T' in *. unfold equalizer_partial_setoid_morphism_form. fold x y₁ y₂. cbn. rewrite !partial_setoid_subst. simplify. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use hyperdoctrine_cut. + exact (ι x ~ ι y₁ ∧ ι x ~ ι y₂). + use conj_intro. * use weaken_left. use from_eq_in_equalizer_partial_setoid. apply hyperdoctrine_hyp. * use weaken_right. use from_eq_in_equalizer_partial_setoid. apply hyperdoctrine_hyp. + use partial_setoid_trans. * exact (ι x). * use partial_setoid_sym. use weaken_left. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. pose (T := equalizer_partial_setoid). pose (T' := X). pose (x := π₂ (tm_var (𝟙 ×h T))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. unfold equalizer_partial_setoid_morphism_form. fold x y. cbn. rewrite !partial_setoid_subst. simplify. use forall_intro. use impl_intro. use weaken_right. use exists_intro. { exact (π₂ (tm_var _)). } unfold x, y ; clear x y. simplify_form. rewrite partial_setoid_subst. simplify. cbn. pose (x := π₂ (tm_var (𝟙 ×h X))). fold x. 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.