Proposition lam_partial_setoid_eq_arg {Γ : ty H} (z z' : tm Γ Z) (f : tm Γ (exp_partial_setoid X Y)) {Δ : form Γ} (p : Δ ⊢ z ~ z') (q : Δ ⊢ f ~ f) (r : Δ ⊢ lam_partial_setoid_form [⟨ z , f ⟩]) : Δ ⊢ lam_partial_setoid_form [⟨ z' , f ⟩]. Proof. use to_lam_partial_setoid_eq. - exact (partial_setoid_refl_r p). - exact (lam_partial_setoid_form_is_function _ _ r). - unfold lam_partial_setoid_eq. rewrite !forall_subst. do 2 use forall_intro. cbn. simplify. pose (γ := π₁ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (x := π₂ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (y := π₂ (tm_var ((Γ ×h X) ×h Y))). fold γ x y. use iff_intro. + use lam_partial_setoid_eq_left. * exact (z [ γ ]tm). * use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ r) _). simplify. apply hyperdoctrine_hyp. * use (partial_setoid_mor_eq_defined φ). ** exact ⟨ x , z' [ γ ]tm ⟩. ** exact y. ** use eq_in_prod_partial_setoid. *** simplify. use weaken_right. refine (hyperdoctrine_cut (partial_setoid_mor_dom_defined φ ⟨ x , z' [ γ ]tm ⟩ y (hyperdoctrine_hyp _)) _). use (hyperdoctrine_cut (eq_in_prod_partial_setoid_l _ _ (hyperdoctrine_hyp _)) _). simplify. apply hyperdoctrine_hyp. *** use weaken_left. simplify. rewrite <- partial_setoid_subst. use hyperdoctrine_proof_subst. use partial_setoid_sym. exact p. ** use (partial_setoid_mor_cod_defined φ). *** exact ⟨ x , z' [ γ ]tm ⟩. *** use weaken_right. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. + assert (Δ [γ] ∧ ⟨ x, y ⟩ ∈ f [γ ]tm ⊢ x ~ x) as lem₁. { refine (hyperdoctrine_cut _ _). * use (partial_setoid_mor_dom_defined φ ⟨ x , z [ γ ]tm ⟩ y _). use (lam_partial_setoid_eq_right (z [ γ ]tm) (f [ γ ]tm) _ x y). ** use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ r) _). simplify. apply hyperdoctrine_hyp. ** use weaken_right. apply hyperdoctrine_hyp. * refine (hyperdoctrine_cut (eq_in_prod_partial_setoid_l _ _ (hyperdoctrine_hyp _)) _). simplify. apply hyperdoctrine_hyp. } assert (Δ [γ] ∧ ⟨ x, y ⟩ ∈ f [γ ]tm ⊢ y ~ y) as lem₂. { use (partial_setoid_mor_cod_defined φ ⟨ x , z [ γ ]tm ⟩ y _). use (lam_partial_setoid_eq_right (z [ γ ]tm) (f [ γ ]tm) _ x y). { use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ r) _). simplify. apply hyperdoctrine_hyp. } use weaken_right. apply hyperdoctrine_hyp. } use (partial_setoid_mor_eq_defined φ). * exact ⟨ x , z [ γ ]tm ⟩. * exact y. * use eq_in_prod_partial_setoid. ** simplify. exact lem₁. ** simplify. use weaken_left. rewrite <- partial_setoid_subst. use hyperdoctrine_proof_subst. exact p. * exact lem₂. * use lam_partial_setoid_eq_right. ** exact (f [ γ ]tm). ** use weaken_left. refine (hyperdoctrine_cut (hyperdoctrine_proof_subst γ r) _). simplify. apply hyperdoctrine_hyp. ** 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.