Proposition partial_setoid_comp_morphism_laws : partial_setoid_morphism_laws partial_setoid_comp_morphism_form. Proof. repeat split. - unfold partial_setoid_mor_dom_defined_law. pose (T := X). pose (T' := Z). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (z := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x z. unfold partial_setoid_comp_morphism_form. simplify. pose (y := π₂ (tm_var (((𝟙 ×h X) ×h Z) ×h Y))). fold y. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. unfold x, y, z. simplify. use weaken_left. apply (partial_setoid_mor_dom_defined φ₁ _ _ (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_cod_defined_law. pose (T := X). pose (T' := Z). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T')))). pose (z := π₂ (tm_var ((𝟙 ×h T) ×h T'))). unfold T, T' in *. fold x z. unfold partial_setoid_comp_morphism_form. simplify. pose (y := π₂ (tm_var (((𝟙 ×h X) ×h Z) ×h Y))). fold y. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. unfold x, y, z. simplify. use weaken_right. apply (partial_setoid_mor_cod_defined φ₂ _ _ (hyperdoctrine_hyp _)). - unfold partial_setoid_mor_eq_defined_law. pose (T := X). pose (T' := Z). 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 (z₁ := π₂ (π₁ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T')))). pose (z₂ := π₂ (tm_var ((((𝟙 ×h T) ×h T) ×h T') ×h T'))). unfold T, T' in *. fold x₁ x₂ z₁ z₂. unfold partial_setoid_comp_morphism_form. simplify. pose (y := π₂ (tm_var (((((𝟙 ×h X) ×h X) ×h Z) ×h Z) ×h Y))). fold y. do 4 use forall_intro. use impl_intro. use weaken_right. do 2 use impl_intro. use hyp_sym. refine (exists_elim _ _) ; [ use weaken_left ; apply hyperdoctrine_hyp | ]. rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify. rewrite !partial_setoid_subst. use exists_intro. + exact (π₂ (tm_var _)). + simplify. use conj_intro. * use hyp_rtrans. use weaken_left. use hyp_sym. use hyp_rtrans. use weaken_left. unfold x₁, x₂, y. simplify. use (partial_setoid_mor_eq_defined φ₁ _ _ (weaken_left (hyperdoctrine_hyp _) _)). ** use weaken_right. use hyperdoctrine_hyp. ** use weaken_left. exact (partial_setoid_mor_cod_defined φ₁ _ _ (hyperdoctrine_hyp _)). * use hyp_ltrans. use weaken_right. use hyp_sym. use hyp_ltrans. use weaken_right. unfold z₁, z₂, y. simplify. use (partial_setoid_mor_eq_defined φ₂ _ _ (weaken_left (hyperdoctrine_hyp _) _)). ** use weaken_left. exact (partial_setoid_mor_dom_defined φ₂ _ _ (hyperdoctrine_hyp _)). ** use weaken_right. use hyperdoctrine_hyp. - unfold partial_setoid_mor_unique_im_law. pose (T := X). pose (T' := Z). 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₂. unfold partial_setoid_comp_morphism_form. simplify. do 3 use forall_intro. use impl_intro. use weaken_right. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify. use impl_intro. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify. rewrite partial_setoid_subst. unfold x, z₁, z₂. clear x z₁ z₂. simplify. pose (x := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h Z) ×h Z) ×h Y) ×h Y))))))). pose (y := π₂ (π₁ (tm_var (((((𝟙 ×h X) ×h Z) ×h Z) ×h Y) ×h Y)))). pose (y' := π₂ (tm_var (((((𝟙 ×h X) ×h Z) ×h Z) ×h Y) ×h Y))). pose (z₁ := π₂ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h Z) ×h Z) ×h Y) ×h Y)))))). pose (z₂ := π₂ (π₁ (π₁ (tm_var (((((𝟙 ×h X) ×h Z) ×h Z) ×h Y) ×h Y))))). fold x y y' z₁ z₂. use (partial_setoid_mor_unique_im φ₂). + exact y. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use (partial_setoid_mor_eq_defined φ₂). * exact y'. * exact z₂. * 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_left. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. * use (partial_setoid_mor_cod_defined φ₂). ** exact y'. ** do 2 use weaken_right. apply hyperdoctrine_hyp. * do 2 use weaken_right. apply hyperdoctrine_hyp. - unfold partial_setoid_mor_hom_exists_law. pose (x := π₂ (tm_var (𝟙 ×h X))). pose (z := π₂ (tm_var ((𝟙 ×h X) ×h Z))). fold x z. use forall_intro. use impl_intro. use weaken_right. use (exists_elim (partial_setoid_mor_hom_exists φ₁ (hyperdoctrine_hyp _))). use weaken_right. pose (y := π₂ (tm_var ((𝟙 ×h X) ×h Y))). fold y. use weaken_cut. + exact (y ~ y). + exact (partial_setoid_mor_cod_defined φ₁ _ _ (hyperdoctrine_hyp _)). + use (exists_elim (partial_setoid_mor_hom_exists φ₂ (weaken_right (hyperdoctrine_hyp _) _))). simplify_form. use hyp_sym. use hyp_rtrans. use weaken_left. use hyp_sym. use exists_intro. * exact (π₂ (tm_var _)). * unfold partial_setoid_comp_morphism_form. simplify. use exists_intro. ** exact (π₂ (π₁ (tm_var _))). ** unfold x, y, z. simplify. apply hyperdoctrine_hyp. 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.