Proposition term_partial_setoid_morphism_laws {H : first_order_hyperdoctrine} {X Y : ty H} (t : tm X Y) : partial_setoid_morphism_laws (term_partial_setoid_morphism_form t). Proof. unfold term_partial_setoid_morphism_form. repeat split. - unfold partial_setoid_mor_dom_defined_law. cbn ; simplify. pose (T := X). pose (T' := Y). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x y. use forall_intro. use forall_intro. use impl_intro. use eq_in_eq_partial_setoid. simplify. apply hyperdoctrine_refl. - unfold partial_setoid_mor_cod_defined_law. cbn ; simplify. pose (T := X). pose (T' := Y). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x y. use forall_intro. use forall_intro. use impl_intro. use eq_in_eq_partial_setoid. simplify. apply hyperdoctrine_refl. - unfold partial_setoid_mor_eq_defined_law. cbn ; simplify. pose (T := X). pose (T' := Y). 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 *. fold x₁ x₂ y₁ y₂. use forall_intro. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use impl_intro. use impl_intro. simplify. use hyperdoctrine_eq_trans. + exact y₁. + use hyperdoctrine_eq_trans. * exact (t [ x₁ ]tm). * use hyperdoctrine_subst_eq. use hyperdoctrine_eq_sym. do 2 use weaken_left. use weaken_right. use from_eq_in_eq_partial_setoid. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. use from_eq_in_eq_partial_setoid. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. cbn ; simplify. pose (T := X). pose (T' := Y). 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 *. fold x y₁ y₂. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use impl_intro. use eq_in_eq_partial_setoid. simplify. use hyperdoctrine_eq_trans. + exact (t [ x ]tm). + use weaken_left. use weaken_right. use hyperdoctrine_eq_sym. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. cbn ; simplify. pose (T := X). pose (T' := Y). pose (x := π₂ (tm_var (𝟙 ×h T))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x y. use forall_intro. use impl_intro. unfold x, y. simplify. use exists_intro. + exact (t [ π₂ (tm_var _) ]tm). + simplify. apply hyperdoctrine_refl. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. 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.