Proposition partial_setoid_pr1_laws : partial_setoid_morphism_laws partial_setoid_pr1_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law. pose (T := prod_partial_setoid X Y). pose (T' := X). 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 weaken_right. cbn. simplify_form. rewrite !partial_setoid_subst. simplify. use eq_in_prod_partial_setoid. + use partial_setoid_refl_l. * exact y. * simplify. use weaken_left. use hyperdoctrine_hyp. + use weaken_right. unfold x. simplify. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law. pose (T := prod_partial_setoid X Y). pose (T' := X). 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 weaken_right. cbn. simplify_form. use weaken_left. rewrite !partial_setoid_subst. simplify. use partial_setoid_refl_r. + exact (π₁ x). + apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law. pose (T := prod_partial_setoid X Y). 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 *. fold x₁ x₂ y₁ y₂. use forall_intro. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use impl_intro. use impl_intro. cbn. simplify_form. rewrite !partial_setoid_subst. simplify. use conj_intro. + use (partial_setoid_trans y₁). * use (partial_setoid_trans (π₁ x₁)). ** do 2 use weaken_left. use partial_setoid_sym. use eq_in_prod_partial_setoid_l. apply hyperdoctrine_hyp. ** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. use eq_in_prod_partial_setoid_r. use partial_setoid_refl_r ; [ | apply hyperdoctrine_hyp ]. - unfold partial_setoid_mor_unique_im_law. pose (T := prod_partial_setoid X Y). pose (T' := X). pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h T) ×h T') ×h T'))))). pose (z₁ := π₂ (π₁ (tm_var (((𝟙 ×h T) ×h T') ×h T')))). pose (z₂ := π₂ (tm_var (((𝟙 ×h T) ×h T') ×h T'))). unfold T, T' in *. fold x z₁ z₂. cbn. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify_form. rewrite !partial_setoid_subst. simplify. use partial_setoid_trans. + exact (π₁ x). + use partial_setoid_sym. use weaken_left. use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. pose (T := prod_partial_setoid X Y). pose (T' := X). pose (x := π₂ (tm_var (𝟙 ×h T))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x y. cbn. use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. use exists_intro. + exact (π₁ (π₂ (tm_var _))). + simplify_form. rewrite !partial_setoid_subst. simplify. use conj_intro. * unfold y. simplify. use eq_in_prod_partial_setoid_l. apply hyperdoctrine_hyp. * use eq_in_prod_partial_setoid_r. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.BinProducts. 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.