Proposition exp_partial_setoid_eq_defined {Γ : ty H} {Δ : form Γ} {f : tm Γ (ℙ (X ×h Y))} (p : Δ ⊢ exp_partial_setoid_is_function [ f ]) {x x' : tm Γ X} (qx : Δ ⊢ x ~ x') {y y' : tm Γ Y} (qy : Δ ⊢ y ~y') (q : Δ ⊢ ⟨ x , y ⟩ ∈ f) : Δ ⊢ ⟨ x' , y' ⟩ ∈ f. Proof. unfold exp_partial_setoid_is_function in p. rewrite !conj_subst in p. pose proof (r := conj_elim_left (conj_elim_right (conj_elim_right p))). clear p. unfold exp_partial_setoid_eq_defined_law in r. rewrite !forall_subst in r. rewrite !impl_subst in r. rewrite !partial_setoid_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. pose proof (r' := forall_elim r x). clear r ; rename r' into r. rewrite !forall_subst in r. rewrite !impl_subst in r. rewrite !partial_setoid_subst in r. rewrite !tripos_in_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !tm_subst_comp in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !tm_subst_comp in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. pose proof (r' := forall_elim r x'). clear r ; rename r' into r. rewrite !forall_subst in r. rewrite !impl_subst in r. rewrite !partial_setoid_subst in r. rewrite !tripos_in_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !tm_subst_comp in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. pose proof (r' := forall_elim r y). clear r ; rename r' into r. rewrite !forall_subst in r. rewrite !impl_subst in r. rewrite !partial_setoid_subst in r. rewrite !tripos_in_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !tm_subst_comp in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !hyperdoctrine_pair_pr2 in r. pose proof (r' := forall_elim r y'). clear r ; rename r' into r. rewrite !impl_subst in r. rewrite !partial_setoid_subst in r. rewrite !tripos_in_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !hyperdoctrine_pair_subst in r. rewrite !hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr2 in r. rewrite !tm_subst_comp in r. rewrite !hyperdoctrine_pr1_subst in r. rewrite !var_tm_subst in r. rewrite !hyperdoctrine_pair_pr1 in r. rewrite !tm_subst_var in r. use (weaken_cut r _). refine (weaken_cut (impl_elim _ (impl_elim _ (impl_elim _ (weaken_right (hyperdoctrine_hyp _) _)))) _). - use weaken_left. exact q. - use weaken_left. exact qy. - use weaken_left. exact qx. - 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.