Proposition lam_partial_setoid_comm : φ = ζ. Proof. use eq_partial_setoid_morphism. - unfold ζ. rewrite <- exp_comm_partial_setoid_eq. pose (x := π₁ (π₁ (tm_var ((X ×h Z) ×h Y)))). pose (y := π₂ (tm_var ((X ×h Z) ×h Y))). pose (z := π₂ (π₁ (tm_var ((X ×h Z) ×h Y)))). assert (φ ⊢ x ~ x) as p₁. { refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined φ ⟨ x , z ⟩ y _) _). { unfold x, y, z. rewrite <- !hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. } use eq_in_prod_partial_setoid_l. unfold x, z. rewrite <- hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. } assert (φ ⊢ z ~ z) as p₂. { refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined φ ⟨ x , z ⟩ y _) _). { unfold x, y, z. rewrite <- !hyperdoctrine_pair_eta. rewrite hyperdoctrine_id_subst. apply hyperdoctrine_hyp. } use eq_in_prod_partial_setoid_r. unfold x, z. rewrite <- hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. } use to_exp_comm_partial_setoid. + exact x. + exact x. + exact z. + exact lam_partial_setoid_comm_form. + fold x. exact p₁. + fold z. exact p₂. + exact p₁. + fold z. exact p₂. + cbn. unfold lam_partial_setoid_form. simplify_form. use conj_intro. * unfold lam_partial_setoid_is_def. simplify_form. rewrite partial_setoid_subst. simplify. repeat use conj_intro. ** exact p₂. ** apply is_function_lam_partial_setoid_comm_form. * apply lam_partial_setoid_eq_lam_partial_setoid_comm_form. + apply is_function_lam_partial_setoid_comm_form. + unfold lam_partial_setoid_comm_form. fold y z. rewrite lam_image_form_eq. unfold x, y, z. rewrite <- !hyperdoctrine_pair_eta. simplify. apply hyperdoctrine_hyp. - unfold ζ. rewrite <- exp_comm_partial_setoid_eq. use from_exp_comm_partial_setoid. pose (Γ := ((((X ×h Z) ×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 Γ))))). unfold Γ in *. fold x₁ x₂ x₃ y z₁ z₂ f. match goal with | [ |- ?Δ' ⊢ _ ] => pose (Δ := Δ') end. fold Δ. assert (Δ ⊢ ⟨ x₂ , y ⟩ ∈ f) as p₁. { use weaken_left. unfold exp_comm_partial_setoid_1. simplify. use weaken_right. apply hyperdoctrine_hyp. } assert (Δ ⊢ x₁ ~ x₂) as p₂. { use weaken_right. use weaken_left. unfold exp_comm_partial_setoid_3. simplify_form. rewrite !partial_setoid_subst. simplify. 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 p₃. { use weaken_left. unfold exp_comm_partial_setoid_1. simplify. use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ ⟨ x₁ , y ⟩ ∈ f) as p₄. { use exp_partial_setoid_eq_defined. + exact p₃. + exact x₂. + use partial_setoid_sym. exact p₂. + exact y. + exact (exp_partial_setoid_cod_defined _ _ p₃ p₁). + exact p₁. } assert (Δ ⊢ φ [⟨ ⟨ x₁ , z₂ ⟩ , y ⟩] ⇔ ⟨ x₁ , y ⟩ ∈ f) as p₅. { do 2 use weaken_right. unfold exp_comm_partial_setoid_2. rewrite !conj_subst. do 2 use weaken_right. unfold lam_partial_setoid ; cbn. simplify. exact (lam_partial_setoid_eq_iff φ z₂ f (hyperdoctrine_hyp _) x₁ y). } assert (Δ ⊢ z₁ ~ z₂) as p₆. { do 2 use weaken_right. unfold exp_comm_partial_setoid_2. rewrite !conj_subst. simplify_form. rewrite !partial_setoid_subst. simplify. use weaken_right. use weaken_left. apply hyperdoctrine_hyp. } assert (Δ ⊢ φ [⟨ ⟨ x₁ , z₂ ⟩ , y ⟩]) as p₇. { use (iff_elim_right p₅). exact p₄. } refine (partial_setoid_mor_eq_defined φ _ _ p₇). + use eq_in_prod_partial_setoid. * simplify. exact (partial_setoid_refl_l p₂). * simplify. use partial_setoid_sym. exact p₆. + exact (exp_partial_setoid_cod_defined _ _ p₃ p₁). 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.