Lemma lam_partial_setoid_unique_left : φ' ⊢ lam_partial_setoid φ. Proof. rewrite p. cbn. pose (z := π₁ (tm_var (Z ×h exp_partial_setoid X Y))). pose (f := π₂ (tm_var (Z ×h exp_partial_setoid X Y))). rewrite <- (hyperdoctrine_id_subst (lam_partial_setoid_form ζ')). rewrite (hyperdoctrine_pair_eta (tm_var (Z ×h exp_partial_setoid X Y))). fold z f. use to_lam_partial_setoid_eq. - use (partial_setoid_mor_dom_defined φ' z f). unfold z, f. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. - assert (φ' ⊢ f ~ f) as q. { use (partial_setoid_mor_cod_defined φ' z f). unfold z, f. rewrite <- hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. } refine (hyperdoctrine_cut q _). use from_eq_in_exp_partial_setoid_function_left. { exact f. } apply hyperdoctrine_hyp. - unfold lam_partial_setoid_eq. rewrite !forall_subst. do 2 use forall_intro. unfold z, f ; clear z f ; cbn -[ζ']. simplify. pose (x := π₂ (π₁ (tm_var (((Z ×h ℙ (X ×h Y)) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((Z ×h ℙ (X ×h Y)) ×h X) ×h Y))). 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))))). fold x y z f. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var (((Z ×h ℙ (X ×h Y)) ×h X) ×h Y))))). fold z f. unfold ζ'. rewrite <- exp_comm_partial_setoid_eq. assert (φ' [⟨ z , f ⟩] ⊢ z ~ z) as q₁. { use (partial_setoid_mor_dom_defined φ' z f). apply hyperdoctrine_hyp. } assert (φ' [⟨ z , f ⟩] ⊢ exp_partial_setoid_is_function [ f ]) as q₂. { use from_eq_in_exp_partial_setoid_function_left. { exact f. } use (partial_setoid_mor_cod_defined φ' z f). apply hyperdoctrine_hyp. } assert (φ' [⟨ z , f ⟩] ∧ ⟨ x , y ⟩ ∈ f ⊢ x ~ x) as q₃. { use (exp_partial_setoid_dom_defined _ _ (weaken_left q₂ _)). { exact y. } use weaken_right. apply hyperdoctrine_hyp. } use iff_intro. + use from_exp_comm_partial_setoid_weaken. unfold x, y, z, f. clear x y z f q₁ q₂ q₃. cbn. simplify. pose (Γ' := (((((Z ×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 Γ'))))). unfold Γ' in * ; clear Γ'. fold x₁ x₂ x₃ y z₁ z₂ f₁ f₂. unfold exp_comm_partial_setoid_1, exp_comm_partial_setoid_2, exp_comm_partial_setoid_3. simplify_form. rewrite !partial_setoid_subst. simplify. pose (Δ := φ' [⟨ z₁, f₁ ⟩] ∧ (exp_partial_setoid_is_function [f₂] ∧ ⟨ x₂, y ⟩ ∈ f₂) ∧ (x₁ ~ x₃ ∧ z₁ ~ z₁ ∧ x₃ ~ x₂) ∧ x₁ ~ x₁ ∧ z₁ ~ z₂ ∧ φ' [⟨ z₂, f₂ ⟩]). assert (Δ ⊢ z₁ ~ z₂) as q₁. { do 4 use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ x₁ ~ x₂) as q₂. { do 2 use weaken_right. use weaken_left. use partial_setoid_trans. - exact x₃. - use weaken_left. apply hyperdoctrine_hyp. - 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 (Δ ⊢ 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. apply hyperdoctrine_hyp. } assert (Δ ⊢ exp_partial_setoid_is_function [f₁]) as q₅. { use exp_partial_setoid_eq_is_function. - exact f₂. - exact q₄. - exact q₃. } 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₆. + unfold exp_comm_partial_setoid. rewrite exists_subst. use exists_intro. { exact ⟨ x , f ⟩. } rewrite !conj_subst. 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₃. ** use weaken_left. 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₃. ** use weaken_left. exact q₁. ** use weaken_left. apply hyperdoctrine_hyp. * simplify. unfold exp_comm_partial_setoid_1. simplify. use conj_intro. ** use weaken_left. 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.