Proposition precategory_of_partial_setoids_laws : is_precategory precategory_data_of_partial_setoids. Proof. use make_is_precategory_one_assoc. - intros X Y φ. use eq_partial_setoid_morphism ; cbn in *. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Y) ×h X)))). pose (x' := π₂ (tm_var ((X ×h Y) ×h X))). pose (y := π₂ (π₁ (tm_var ((X ×h Y) ×h X)))). fold x x' y. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((X ×h Y) ×h X)))). fold x y. use (partial_setoid_mor_eq_defined φ). * exact x'. * exact y. * use weaken_left. use partial_setoid_sym. apply hyperdoctrine_hyp. * use weaken_right. exact (partial_setoid_mor_cod_defined φ _ _ (hyperdoctrine_hyp _)). * use weaken_right. apply hyperdoctrine_hyp. + rewrite partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Y) ×h X)))). pose (x' := π₂ (tm_var ((X ×h Y) ×h X))). pose (y := π₂ (π₁ (tm_var ((X ×h Y) ×h X)))). fold x x' y. use exists_intro. * exact (π₁ (tm_var (X ×h Y))). * simplify_form. rewrite partial_setoid_subst. unfold x, x', y ; clear x x' y. simplify. use conj_intro. ** use (partial_setoid_mor_dom_defined φ _ (π₂ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. ** rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. - intros X Y φ. use eq_partial_setoid_morphism ; cbn in *. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. rewrite partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y := π₂ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y' := π₂ (tm_var ((X ×h Y) ×h Y))). fold x y y'. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var ((X ×h Y) ×h Y)))). fold x y. use (partial_setoid_mor_eq_defined φ). * exact x. * exact y'. * use weaken_left. exact (partial_setoid_mor_dom_defined φ _ _ (hyperdoctrine_hyp _)). * use weaken_right. apply hyperdoctrine_hyp. * use weaken_left. apply hyperdoctrine_hyp. + rewrite partial_setoid_subst. simplify. pose (x := π₁ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y := π₂ (π₁ (tm_var ((X ×h Y) ×h Y)))). pose (y' := π₂ (tm_var ((X ×h Y) ×h Y))). fold x y y'. use exists_intro. * exact (π₂ (tm_var (X ×h Y))). * simplify_form. rewrite partial_setoid_subst. unfold x, y, y' ; clear x y y'. simplify. use conj_intro. ** rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. ** use (partial_setoid_mor_cod_defined φ (π₁ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. - intros W X Y Z φ₁ φ₂ φ₃. use eq_partial_setoid_morphism ; cbn in *. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h Z) ×h X) ×h Y))))). pose (x := π₂ (π₁ (tm_var (((W ×h Z) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((W ×h Z) ×h X) ×h Y))). pose (z := π₂ (π₁ (π₁ (tm_var (((W ×h Z) ×h X) ×h Y))))). fold w x y z. use exists_intro. * exact y. * simplify. fold z. use conj_intro. ** use exists_intro. *** exact x. *** simplify. fold w. use conj_intro. **** use weaken_left. apply hyperdoctrine_hyp. **** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. ** do 2 use weaken_right. apply hyperdoctrine_hyp. + use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. simplify_form. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h Z) ×h Y) ×h X))))). pose (x := π₂ (tm_var (((W ×h Z) ×h Y) ×h X))). pose (y := π₂ (π₁ (tm_var (((W ×h Z) ×h Y) ×h X)))). pose (z := π₂ (π₁ (π₁ (tm_var (((W ×h Z) ×h Y) ×h X))))). fold w x y z. use exists_intro. * exact x. * simplify. fold w. use conj_intro. ** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. ** use exists_intro. *** exact y. *** simplify. fold z. use conj_intro. **** do 2 use weaken_right. apply hyperdoctrine_hyp. **** use weaken_left. 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.