Proposition is_function_lam_image_form (Δ : form (𝟙 ×h Z)) (p : Δ ⊢ π₂ (tm_var _) ~ π₂ (tm_var _)) : Δ ⊢ exp_partial_setoid_is_function [{{lam_image_form}}]. Proof. unfold exp_partial_setoid_is_function. simplify_form. repeat use conj_intro. - unfold exp_partial_setoid_dom_defined_law. simplify_form. do 2 use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite partial_setoid_subst. 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. refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined φ ⟨ x , z ⟩ y (hyperdoctrine_hyp _)) _). refine (hyperdoctrine_cut (eq_in_prod_partial_setoid_l _ _ (hyperdoctrine_hyp _)) _). simplify. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_cod_defined_law. simplify_form. do 2 use forall_intro. use impl_intro. use weaken_right. simplify_form. rewrite partial_setoid_subst. 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. } use (partial_setoid_mor_cod_defined φ ⟨ x , z ⟩ y _). rewrite lam_image_form_eq. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_eq_defined_law. simplify_form. do 4 use forall_intro. do 3 use impl_intro. simplify_form. rewrite !partial_setoid_subst. simplify. pose (Γ := ((((𝟙 ×h Z) ×h X) ×h X) ×h Y) ×h Y). pose (x₁ := π₂ (π₁ (π₁ (π₁ (tm_var Γ))))). pose (x₂ := π₂ (π₁ (π₁ (tm_var Γ)))). pose (y₁ := π₂ (π₁ (tm_var Γ))). pose (y₂ := π₂ (tm_var Γ)). pose (z := π₂ (π₁ (π₁ (π₁ (π₁ (tm_var Γ)))))). unfold Γ in * ; clear Γ. fold x₁ x₂ y₁ y₂ z. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Z) ×h X) ×h X) ×h Y) ×h Y))))))). fold z. assert (π₁ (π₁ (π₁ (π₁ (π₁ (tm_var (((((𝟙 ×h Z) ×h X) ×h X) ×h Y) ×h Y)))))) = !!) as ->. { apply hyperdoctrine_unit_eta. } rewrite !lam_image_form_eq. use (partial_setoid_mor_eq_defined φ). + exact ⟨ x₁ , z ⟩. + exact y₁. + use eq_in_prod_partial_setoid. * simplify. do 2 use weaken_left. use weaken_right. apply hyperdoctrine_hyp. * simplify. do 3 use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst ⟨ !! , z ⟩ p) _). rewrite partial_setoid_subst. simplify. apply hyperdoctrine_hyp. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_unique_im_law. simplify_form. do 3 use forall_intro. use impl_intro. use weaken_right. use impl_intro. simplify_form. rewrite partial_setoid_subst. simplify. pose (z := π₂ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y)))))). pose (x := π₂ (π₁ (π₁ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y))))). pose (y := π₂ (π₁ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y)))). pose (y' := π₂ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y))). fold x y y' z. rewrite (hyperdoctrine_pair_eta (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y)))))). fold z. assert (π₁ (π₁ (π₁ (π₁ (tm_var ((((𝟙 ×h Z) ×h X) ×h Y) ×h Y))))) = !!) as ->. { apply hyperdoctrine_unit_eta. } rewrite !lam_image_form_eq. use (partial_setoid_mor_unique_im φ). + exact ⟨ x , z ⟩. + use weaken_left. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. - unfold exp_partial_setoid_im_exists_law. simplify_form. use forall_intro. use impl_intro. rewrite partial_setoid_subst. simplify. pose (x := π₂ (tm_var ((𝟙 ×h Z) ×h X))). pose (z := π₂ (π₁ (tm_var ((𝟙 ×h Z) ×h X)))). fold x. refine (weaken_cut _ _). { use weaken_left. exact (hyperdoctrine_proof_subst (π₁ (tm_var ((𝟙 ×h Z) ×h X))) p). } use hyp_ltrans. use weaken_right. rewrite partial_setoid_subst. simplify. fold z. use (exists_elim (partial_setoid_mor_hom_exists φ (x := ⟨ x , z ⟩) _)). + use eq_in_prod_partial_setoid. * simplify. use weaken_left. apply hyperdoctrine_hyp. * simplify. use weaken_right. apply hyperdoctrine_hyp. + unfold x, z ; clear x z. rewrite exists_subst. 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))))). use exists_intro. { exact y. } cbn. simplify_form. rewrite !partial_setoid_subst. simplify. 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. use weaken_right. 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.