Proposition to_exp_comm_partial_setoid (Δ : form ((X ×h Z) ×h Y)) (x := π₁ (π₁ (tm_var ((X ×h Z) ×h Y)))) (y := π₂ (tm_var ((X ×h Z) ×h Y))) (z := π₂ (π₁ (tm_var ((X ×h Z) ×h Y)))) (t₁ t₂ : tm ((X ×h Z) ×h Y) X) (t₃ : tm ((X ×h Z) ×h Y) Z) (f : tm ((X ×h Z) ×h Y) (ℙ (X ×h Y))) (p₁ : Δ ⊢ x ~ t₂) (p₂ : Δ ⊢ z ~ z) (p₃ : Δ ⊢ t₂ ~ t₁) (p₄ : Δ ⊢ z ~ t₃) (p₅ : Δ ⊢ ψ [⟨ t₃ , f ⟩]) (p₆ : Δ ⊢ exp_partial_setoid_is_function [ f ]) (p₇ : Δ ⊢ ⟨ t₁, y ⟩ ∈ f) : Δ ⊢ exp_comm_partial_setoid. Proof. cbn in Δ. use exists_intro. { exact ⟨ t₁ , f ⟩. } simplify_form. repeat use conj_intro. - use exists_intro. { exact t₂. } unfold exp_comm_partial_setoid_3. cbn. simplify_form. rewrite !partial_setoid_subst. simplify. fold x y z. repeat use conj_intro. + exact p₁. + exact p₂. + exact p₃. - use exists_intro. { exact t₃. } unfold exp_comm_partial_setoid_2. simplify_form. rewrite !partial_setoid_subst. simplify. fold x y z. repeat use conj_intro. + exact (partial_setoid_refl_l p₁). + exact p₄. + exact p₅. - unfold exp_comm_partial_setoid_1. simplify. fold y. repeat use conj_intro. + exact p₆. + exact 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.