Proposition pair_partial_setoid_morphism_laws : partial_setoid_morphism_laws pair_partial_setoid_morphism_form. Proof. unfold pair_partial_setoid_morphism_form. repeat split. - unfold partial_setoid_mor_dom_defined_law. cbn ; simplify. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). pose (x := π₁ (π₂ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). pose (y := π₂ (π₂ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). fold w x y. do 2 use forall_intro. use impl_intro. do 2 use weaken_right. use (partial_setoid_mor_dom_defined ψ w y). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_cod_defined_law. cbn ; simplify. pose (w := π₂ (π₁ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). pose (x := π₁ (π₂ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). pose (y := π₂ (π₂ (tm_var ((𝟙 ×h W) ×h X ×h Y)))). fold w x y. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use eq_in_prod_partial_setoid ; fold x y. + use weaken_left. use (partial_setoid_mor_cod_defined φ w x). apply hyperdoctrine_hyp. + use weaken_right. use (partial_setoid_mor_cod_defined ψ w y). apply hyperdoctrine_hyp. - unfold partial_setoid_mor_eq_defined_law. pose (T := W). pose (T' := prod_partial_setoid X Y). pose (w₁ := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T')))))). pose (w₂ := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T'))))). pose (xy₁ := π₂ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T')))). pose (xy₂ := π₂ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T'))). unfold T, T' in *. fold w₁ w₂ xy₁ xy₂. simplify. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use conj_intro. + use hyp_rtrans. use weaken_left. use (partial_setoid_mor_eq_defined φ). * exact w₁. * exact (π₁ xy₁). * do 2 use weaken_left. apply hyperdoctrine_hyp. * use weaken_left. use weaken_right. use eq_in_prod_partial_setoid_l. apply hyperdoctrine_hyp. * use weaken_right. apply hyperdoctrine_hyp. + use hyp_sym. use hyp_ltrans. use weaken_right. use (partial_setoid_mor_eq_defined ψ). * exact w₁. * exact (π₂ xy₁). * use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * do 2 use weaken_right. use eq_in_prod_partial_setoid_r. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. pose (T := W). pose (T' := prod_partial_setoid X Y). 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₂. simplify. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. use eq_in_prod_partial_setoid. + use hyp_rtrans. use weaken_left. use hyp_sym. use hyp_rtrans. use weaken_left. use (partial_setoid_mor_unique_im φ). * exact x. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. + use hyp_ltrans. use weaken_right. use hyp_sym. use hyp_ltrans. use weaken_right. use (partial_setoid_mor_unique_im ψ). * exact x. * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. pose (T := W). pose (T' := prod_partial_setoid X Y). 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. use (exists_elim (partial_setoid_mor_hom_exists φ (hyperdoctrine_hyp _))). rewrite partial_setoid_subst. use (exists_elim (partial_setoid_mor_hom_exists ψ (weaken_left (hyperdoctrine_hyp _) _))). unfold x, y. simplify_form. use hyp_ltrans. use weaken_right. use exists_intro. + exact (⟨ π₂ (π₁ (tm_var _)) , π₂ (tm_var _) ⟩). + unfold x, y. simplify. 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.