Proposition pair_partial_setoid_morphism_unique : χ = pair_partial_setoid_morphism. Proof. use eq_partial_setoid_morphism ; cbn. - use conj_intro. + refine (from_eq_partial_setoid_morphism_f p₁ _) ; cbn. simplify_form. use exists_intro. * exact (π₂ (tm_var _)). * simplify_form. rewrite !partial_setoid_subst. simplify. rewrite <- hyperdoctrine_pair_eta. simplify_form. repeat (use conj_intro). ** apply hyperdoctrine_hyp. ** use eq_in_prod_partial_setoid_l. use (partial_setoid_mor_cod_defined χ (π₁ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. simplify_form. apply hyperdoctrine_hyp. ** use eq_in_prod_partial_setoid_r. use (partial_setoid_mor_cod_defined χ (π₁ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. simplify_form. apply hyperdoctrine_hyp. + refine (from_eq_partial_setoid_morphism_f p₂ _) ; cbn. simplify_form. use exists_intro. * exact (π₂ (tm_var _)). * simplify_form. rewrite !partial_setoid_subst. simplify. rewrite <- hyperdoctrine_pair_eta. simplify_form. repeat (use conj_intro). ** apply hyperdoctrine_hyp. ** use eq_in_prod_partial_setoid_l. use (partial_setoid_mor_cod_defined χ (π₁ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. simplify_form. apply hyperdoctrine_hyp. ** use eq_in_prod_partial_setoid_r. use (partial_setoid_mor_cod_defined χ (π₁ (tm_var _))). rewrite <- hyperdoctrine_pair_eta. simplify_form. apply hyperdoctrine_hyp. - pose (w := π₁ (tm_var (W ×h X ×h Y))). pose (x := π₁ (π₂ (tm_var (W ×h X ×h Y)))). pose (y := π₂ (π₂ (tm_var (W ×h X ×h Y)))). pose (Δ := φ [⟨ w, x ⟩] ∧ ψ [⟨ w, y ⟩]). fold w x y Δ. assert (Δ ⊢ φ [⟨ w , x ⟩]) as q. { use weaken_left. apply hyperdoctrine_hyp. } use (weaken_cut (from_eq_partial_setoid_morphism_b p₁ q)). cbn. simplify_form. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite !partial_setoid_subst. unfold Δ, w, x, y. simplify. clear q w x y Δ. use hyp_ltrans. use weaken_right. refine (weaken_cut (weaken_left (from_eq_partial_setoid_morphism_b p₂ (hyperdoctrine_hyp _)) _) _). use hyp_ltrans. use weaken_right. cbn. simplify. use hyp_sym. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). rewrite conj_subst. use hyp_ltrans. use weaken_right. simplify_form. rewrite !partial_setoid_subst. simplify. pose (w := π₁ (π₁ (π₁ (tm_var (((W ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))))). pose (xy₁:= π₂ (π₁ (tm_var (((W ×h X ×h Y) ×h X ×h Y) ×h X ×h Y)))). pose (xy₂ := π₂ (π₁ (π₁ (tm_var (((W ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))))). pose (xy₃ := π₂ (tm_var (((W ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))). fold w xy₁ xy₂ xy₃. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var (((W ×h X ×h Y) ×h X ×h Y) ×h X ×h Y))))). fold w xy₂. use (partial_setoid_mor_eq_defined χ). + exact w. + exact xy₁. + use (partial_setoid_mor_dom_defined χ _ xy₁). do 2 use weaken_left. apply hyperdoctrine_hyp. + use eq_in_prod_partial_setoid. * use weaken_left. use weaken_right. use weaken_left. apply hyperdoctrine_hyp. * use partial_setoid_trans. ** exact (π₂ xy₃). ** use eq_in_prod_partial_setoid_r. use (partial_setoid_mor_unique_im χ). *** exact w. *** do 2 use weaken_left. apply hyperdoctrine_hyp. *** use weaken_right. use weaken_left. apply hyperdoctrine_hyp. ** do 3 use weaken_right. apply hyperdoctrine_hyp. + do 2 use weaken_left. 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.