Proposition partial_setoid_morphism_to_terminal_laws {H : first_order_hyperdoctrine} (X : partial_setoid H) : partial_setoid_morphism_laws (partial_setoid_morphism_to_terminal_form X). Proof. unfold partial_setoid_morphism_to_terminal_form. repeat split. - unfold partial_setoid_mor_dom_defined_law. cbn ; simplify. rewrite partial_setoid_subst. simplify. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h 𝟙)))). fold x. use forall_intro. use forall_intro. use impl_intro. use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law. cbn ; simplify. rewrite partial_setoid_subst. simplify. pose (x := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h 𝟙)))). pose (y := π₂ (tm_var ((𝟙 ×h X) ×h 𝟙))). fold x y. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use eq_in_eq_partial_setoid. apply hyperdoctrine_refl. - unfold partial_setoid_mor_eq_defined_law. cbn ; simplify. rewrite !partial_setoid_subst. simplify. pose (T := X). pose (T' := 𝟙 : ty H). 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₂. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. do 2 use weaken_left. use partial_setoid_refl_r. { exact x₁. } apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. cbn ; simplify. rewrite !partial_setoid_subst. simplify. pose (T := X). pose (T' := 𝟙 : ty H). 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₂. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use eq_in_eq_partial_setoid. use hyperdoctrine_unit_tm_eq. - unfold partial_setoid_mor_hom_exists_law. cbn ; simplify. rewrite !partial_setoid_subst. simplify. pose (T := X). pose (T' := 𝟙 : ty H). 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. use weaken_right. use exists_intro. + exact !!. + rewrite partial_setoid_subst. simplify. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. 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. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects.