Proposition lam_partial_setoid_eq_lam_partial_setoid_comm_form (z := π₂ (π₁ (tm_var ((X ×h Z) ×h Y)))) : φ ⊢ (lam_partial_setoid_eq φ) [⟨ z , lam_partial_setoid_comm_form ⟩]. Proof. unfold lam_partial_setoid_comm_form. simple refine (hyperdoctrine_cut _ (hyperdoctrine_cut (hyperdoctrine_proof_subst ⟨ !! , π₂ (π₁ (tm_var _)) ⟩ (lam_partial_setoid_eq_image_form φ (π₂ (tm_var _) ~ π₂ (tm_var _)))) _)). - clear z. rewrite partial_setoid_subst. simplify. 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)))). fold z. 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. + refine (hyperdoctrine_cut (eq_in_prod_partial_setoid_r _ _ (hyperdoctrine_hyp _)) _). simplify. apply hyperdoctrine_hyp. - simplify. 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.