Proposition lam_partial_setoid_eq_image_form (Δ : form (𝟙 ×h Z)) : Δ ⊢ lam_partial_setoid_eq [⟨ π₂ (tm_var (𝟙 ×h Z)) , {{lam_image_form}} ⟩]. Proof. unfold lam_partial_setoid_eq. rewrite !forall_subst. do 2 use forall_intro. cbn. simplify. pose (x := π₂ (π₁ (tm_var (((𝟙 ×h Z) ×h X) ×h Y)))). pose (y := π₂ (tm_var (((𝟙 ×h Z) ×h X) ×h Y))). pose (z := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h Z) ×h X) ×h Y))))). fold x y z. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (tm_var (((𝟙 ×h Z) ×h X) ×h Y))))). fold z. assert (π₁ (π₁ (π₁ (tm_var (((𝟙 ×h Z) ×h X) ×h Y)))) = !!) as ->. { apply hyperdoctrine_unit_eta. } rewrite lam_image_form_eq. apply iff_refl. 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.