Proposition equalizer_per_axioms : per_axioms equalizer_per_form. Proof. repeat split ; cbn. - pose (x := π₁ (tm_var (X ×h X))). pose (x' := π₂ (tm_var (X ×h X))). pose (y := π₂ (tm_var ((X ×h X) ×h Y))). fold x x' y. unfold per_symm_axiom. use forall_intro. use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite !partial_setoid_subst. unfold x, x', y ; clear x x' y. simplify. use conj_intro. + pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h X)))). pose (x' := π₂ (tm_var ((𝟙 ×h X) ×h X))). fold x x'. use weaken_left. use partial_setoid_sym. apply hyperdoctrine_hyp. + use (exists_elim (weaken_right (hyperdoctrine_hyp _) _)). use hyp_sym. simplify_form. rewrite partial_setoid_subst. use hyp_rtrans. use weaken_left. use exists_intro. * exact (π₂ (tm_var _)). * simplify. pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h Y))))). pose (x' := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h X) ×h X) ×h Y))). fold x x' y. use conj_intro. ** use (partial_setoid_mor_eq_defined φ). *** exact x. *** exact y. *** use weaken_right. apply hyperdoctrine_hyp. *** do 2 use weaken_left. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). *** do 2 use weaken_left. apply hyperdoctrine_hyp. ** use (partial_setoid_mor_eq_defined ψ). *** exact x. *** exact y. *** use weaken_right. apply hyperdoctrine_hyp. *** do 2 use weaken_left. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). *** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. - unfold per_trans_axiom. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h X))))). pose (x₂ := π₂ (π₁ (tm_var (((𝟙 ×h X) ×h X) ×h X)))). pose (x₃ := π₂ (tm_var (((𝟙 ×h X) ×h X) ×h X))). fold x₁ x₂ x₃. do 3 use forall_intro. use impl_intro. use weaken_right. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. use impl_intro. use hyp_rtrans. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. use conj_intro. + unfold x₁, x₂, x₃ ; clear x₁ x₂ x₃. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))))))). pose (x₂ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₃ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))). fold x₁ x₂ x₃ y₁ y₂. use partial_setoid_trans. * exact x₂. * do 3 use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use exists_intro. * exact (π₂ (tm_var _)). * unfold x₁, x₂, x₃ ; clear x₁ x₂ x₃. simplify_form. rewrite !partial_setoid_subst. simplify. pose (x₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))))))). pose (x₂ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y)))))). pose (x₃ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))))). pose (y₁ := π₂ (π₁ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y)))). pose (y₂ := π₂ (tm_var (((((𝟙 ×h X) ×h X) ×h X) ×h Y) ×h Y))). fold x₁ x₂ x₃ y₁ y₂. use conj_intro. ** use (partial_setoid_mor_eq_defined φ). *** exact x₂. *** exact y₂. *** use partial_setoid_sym. do 3 use weaken_left. apply hyperdoctrine_hyp. *** do 2 use weaken_right. use (partial_setoid_mor_cod_defined ψ x₂). apply hyperdoctrine_hyp. *** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. ** use (partial_setoid_mor_eq_defined ψ). *** exact x₂. *** exact y₂. *** use partial_setoid_sym. do 3 use weaken_left. apply hyperdoctrine_hyp. *** do 2 use weaken_right. use (partial_setoid_mor_cod_defined ψ x₂). apply hyperdoctrine_hyp. *** do 2 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.