Proposition from_exp_comm_partial_setoid (χ : form ((X ×h Z) ×h Y)) (Γ := ((((X ×h Z) ×h Y) ×h X ×h ℙ (X ×h Y)) ×h X) ×h Z) (x₁ := π₁ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))) (x₂ := π₁ (π₂ (π₁ (π₁ (tm_var Γ))))) (x₃ := π₂ (π₁ (tm_var Γ))) (y := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))) (z₁ := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))) (z₂ := π₂ (tm_var Γ)) (f := π₂ (π₂ (π₁ (π₁ (tm_var Γ))))) (p : (exp_comm_partial_setoid_1 [ ⟨ ⟨ ⟨ x₁ , z₁ ⟩ , y ⟩ , ⟨ x₂ , f ⟩ ⟩ ] ∧ exp_comm_partial_setoid_3 [ ⟨ ⟨ ⟨ ⟨ x₁ , z₁ ⟩ , y ⟩ , ⟨ x₂ , f ⟩ ⟩ , x₃ ⟩ ] ∧ exp_comm_partial_setoid_2 [ ⟨ ⟨ ⟨ ⟨ x₁ , z₁ ⟩ , y ⟩ , ⟨ x₂ , f ⟩ ⟩ , z₂ ⟩ ] ⊢ χ [ ⟨ ⟨ x₁ , z₁ ⟩ , y ⟩ ])) : exp_comm_partial_setoid ⊢ χ. Proof. unfold exp_comm_partial_setoid. use (exists_elim (hyperdoctrine_hyp _)). use weaken_right. pose (Δ := (∃h exp_comm_partial_setoid_3 ∧ ∃h exp_comm_partial_setoid_2 ∧ exp_comm_partial_setoid_1)). assert (Δ ⊢ ∃h exp_comm_partial_setoid_3) as q. { use weaken_left. apply hyperdoctrine_hyp. } unfold Δ in q. use (exists_elim q) ; clear q. simplify_form. use hyp_ltrans. use weaken_right. use hyp_ltrans. use (exists_elim (weaken_left (hyperdoctrine_hyp _) _)). simplify_form. use hyp_ltrans. use weaken_right. simplify. refine (hyperdoctrine_cut (hyperdoctrine_cut _ p) _). - fold Γ. use hyp_ltrans. unfold x₁, x₂, x₃, y, z₁, z₂, f. rewrite <- !hyperdoctrine_pair_eta. apply hyperdoctrine_hyp. - fold Γ. unfold x₁, z₁, y. rewrite <- !hyperdoctrine_pair_eta. 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.