Lemma lam_partial_setoid_unique_right : lam_partial_setoid φ ⊢ φ'. Proof. rewrite p. use (exists_elim (partial_setoid_mor_hom_exists φ' _)). - exact (π₁ (tm_var _)). - use (partial_setoid_mor_dom_defined (lam_partial_setoid ζ')). { exact (π₂ (tm_var _)). } rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. - cbn. simplify. pose (z := π₁ (π₁ (tm_var ((Z ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y))))). pose (f := π₂ (π₁ (tm_var ((Z ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y))))). pose (g := π₂ (tm_var ((Z ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)))). fold z f g. rewrite (hyperdoctrine_pair_eta (π₁ (tm_var _))). fold z f. assert ((lam_partial_setoid_form ζ') [⟨ z , f ⟩] ∧ φ' [⟨ z , g ⟩] ⊢ z ~ z) as q₁. { use weaken_right. use (partial_setoid_mor_dom_defined φ' z g). apply hyperdoctrine_hyp. } use (partial_setoid_mor_eq_defined φ'). + exact z. + exact g. + exact q₁. + use eq_in_exp_partial_setoid. * use weaken_right. refine (hyperdoctrine_cut _ _). { use (partial_setoid_mor_cod_defined φ' z g). apply hyperdoctrine_hyp. } exact (from_eq_in_exp_partial_setoid_function_left _ _ (hyperdoctrine_hyp _)). * unfold exp_partial_setoid_eq. rewrite !forall_subst. do 2 use forall_intro. unfold z, f, g. clear z f g q₁. simplify. pose (Γ := (((Z ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h X) ×h Y). pose (x := π₂ (π₁ (tm_var Γ))). pose (y := π₂ (tm_var Γ)). pose (z := π₁ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (f := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (g := π₂ (π₁ (π₁ (tm_var Γ)))). unfold Γ in * ; clear Γ. fold x y z f g. pose (Δ := (lam_partial_setoid_form ζ') [⟨ z, f ⟩] ∧ φ' [⟨ z, g ⟩]). assert (Δ ⊢ (lam_partial_setoid_form ζ') [⟨ z, f ⟩]) as q. { use weaken_left. apply hyperdoctrine_hyp. } refine (iff_trans _ (lam_partial_setoid_eq_iff _ _ _ q x y)). unfold Δ. unfold ζ'. rewrite <- exp_comm_partial_setoid_eq. use iff_intro. ** unfold exp_comm_partial_setoid. rewrite !exists_subst. use exists_intro. { exact ⟨ x , g ⟩. } rewrite !conj_subst. match goal with | [ |- ?Δ' ⊢ _ ] => pose (Δ'' := Δ') end. assert (Δ'' ⊢ z ~ z) as q₁. { unfold Δ''. use weaken_left. use weaken_right. use (partial_setoid_mor_dom_defined φ' z g). apply hyperdoctrine_hyp. } assert (Δ'' ⊢ exp_partial_setoid_is_function [g]) as q₂. { use weaken_left. use weaken_right. refine (hyperdoctrine_cut _ _). { use (partial_setoid_mor_cod_defined φ' z g). apply hyperdoctrine_hyp. } exact (from_eq_in_exp_partial_setoid_function_left _ _ (hyperdoctrine_hyp _)). } assert (Δ'' ⊢ x ~ x) as q₃. { use (exp_partial_setoid_dom_defined _ _ q₂). { exact y. } use weaken_right. apply hyperdoctrine_hyp. } repeat use conj_intro. *** rewrite !exists_subst. use exists_intro. { exact x. } simplify. unfold exp_comm_partial_setoid_3. simplify_form. rewrite !partial_setoid_subst. simplify. repeat use conj_intro. **** exact q₃. **** exact q₁. **** exact q₃. *** rewrite !exists_subst. use exists_intro. { exact z. } simplify. unfold exp_comm_partial_setoid_2. simplify_form. rewrite !partial_setoid_subst. simplify. repeat use conj_intro. **** exact q₃. **** exact q₁. **** use weaken_left. use weaken_right. apply hyperdoctrine_hyp. *** unfold exp_comm_partial_setoid_1. simplify. use conj_intro. **** exact q₂. **** use weaken_right. apply hyperdoctrine_hyp. ** clear Δ q. unfold x, y, z, f, g. use from_exp_comm_partial_setoid_weaken. cbn. simplify. clear x y z f g. pose (Γ := ((((((Z ×h ℙ (X ×h Y)) ×h ℙ (X ×h Y)) ×h X) ×h Y) ×h X ×h ℙ (X ×h Y)) ×h X) ×h Z). pose (x₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))). pose (x₂ := π₁ (π₂ (π₁ (π₁ (tm_var Γ))))). pose (x₃ := π₂ (π₁ (tm_var Γ))). pose (y := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (z₁ := π₁ (π₁ (π₁ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))))). pose (z₂ := π₂ (tm_var Γ)). pose (f₁ := π₂ (π₁ (π₁ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))))). pose (f₂ := π₂ (π₁ (π₁ (π₁ (π₁ (π₁ (tm_var Γ))))))). pose (f₃ := π₂ (π₂ (π₁ (π₁ (tm_var Γ))))). unfold Γ in *. fold x₁ x₂ x₃ y z₁ z₂ f₁ f₂ f₃. unfold exp_comm_partial_setoid_1. unfold exp_comm_partial_setoid_2. unfold exp_comm_partial_setoid_3. simplify_form. rewrite !partial_setoid_subst. simplify. match goal with | [ |- ?Δ' ⊢ _ ] => pose (Δ := Δ') end. assert (Δ ⊢ x₁ ~ x₂) as q₁. { use partial_setoid_trans. - exact x₃. - do 2 use weaken_right. do 2 use weaken_left. apply hyperdoctrine_hyp. - do 2 use weaken_right. use weaken_left. do 2 use weaken_right. apply hyperdoctrine_hyp. } assert (Δ ⊢ exp_partial_setoid_is_function [f₃]) as q₂. { use weaken_right. do 2 use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ z₁ ~ z₂) as q₃. { do 4 use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ exp_partial_setoid_eq[⟨ f₃ , f₂ ⟩]) as q₄. { use from_eq_in_exp_partial_setoid_function_eq. use (partial_setoid_mor_unique_im φ'). - exact z₁. - use (partial_setoid_mor_eq_defined φ'). + exact z₂. + exact f₃. + use partial_setoid_sym. exact q₃. + use eq_in_exp_partial_setoid. * exact q₂. * apply exp_partial_setoid_eq_refl. + do 5 use weaken_right. apply hyperdoctrine_hyp. - use weaken_left. use weaken_right. apply hyperdoctrine_hyp. } assert (Δ ⊢ ⟨ x₂, y ⟩ ∈ f₃) as q₅. { use weaken_right. use weaken_left. use weaken_right. apply hyperdoctrine_hyp. } assert (Δ ⊢ y ~ y) as q₆. { exact (exp_partial_setoid_cod_defined _ _ q₂ q₅). } use (from_exp_partial_setoid_eq _ _ q₄). use (exp_partial_setoid_eq_defined _ _ q₂). *** exact x₂. *** use partial_setoid_sym. exact q₁. *** exact y. *** exact q₆. *** exact q₅. + use weaken_right. 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.Tripos. Require Import UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate. 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.PERBinProducts. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialPER. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEval. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialLam.