Proposition partial_setoid_mor_cod_defined (φ : partial_setoid_morphism) {Γ : ty H} {Δ : form Γ} (x : tm Γ X) (y : tm Γ Y) (p : Δ ⊢ φ [ ⟨ x , y ⟩ ]) : Δ ⊢ y ~ y. Proof. pose (q := pr122 φ). unfold partial_setoid_mor_cod_defined_law in q ; cbn in q. pose (x' := π₂ (π₁ (tm_var ((𝟙 ×h X) ×h Y)))). pose (y' := π₂ (tm_var ((𝟙 ×h X) ×h Y))). fold x' y' in q. pose proof (hyperdoctrine_proof_subst (!! : tm Γ 𝟙) q) as q'. clear q. rename q' into q. rewrite truth_subst in q. rewrite !forall_subst in q. rewrite impl_subst in q. rewrite partial_setoid_subst in q. rewrite !hyperdoctrine_pair_subst in q. rewrite !hyperdoctrine_unit_tm_subst in q. rewrite !hyperdoctrine_comp_subst in q. rewrite !hyperdoctrine_pair_subst in q. unfold x', y' in q ; clear x' y'. rewrite !hyperdoctrine_pr2_subst in q. rewrite !hyperdoctrine_pr1_subst in q. rewrite !var_tm_subst in q. rewrite hyperdoctrine_pair_pr1 in q. rewrite !hyperdoctrine_pair_pr2 in q. pose (x' := π₂ (π₁ (tm_var ((Γ ×h X) ×h Y)))). pose (y' := π₂ (tm_var ((Γ ×h X) ×h Y))). fold x' y' in q. pose proof (forall_elim q x) as q'. clear q. rename q' into q. rewrite !forall_subst in q. rewrite impl_subst in q. rewrite partial_setoid_subst in q. rewrite !hyperdoctrine_pair_subst in q. rewrite var_tm_subst in q. rewrite !hyperdoctrine_comp_subst in q. rewrite !hyperdoctrine_pair_subst in q. unfold x', y' in q ;clear x' y'. rewrite !hyperdoctrine_pr2_subst in q. rewrite hyperdoctrine_pr1_subst in q. rewrite var_tm_subst in q. rewrite hyperdoctrine_pair_pr1 in q. rewrite !hyperdoctrine_pair_pr2 in q. pose proof (forall_elim q y) as q'. clear q. rename q' into q. rewrite impl_subst in q. rewrite partial_setoid_subst in q. rewrite !hyperdoctrine_comp_subst in q. rewrite !hyperdoctrine_pair_subst in q. rewrite !hyperdoctrine_pr2_subst in q. rewrite var_tm_subst in q. rewrite !hyperdoctrine_pair_pr2 in q. rewrite tm_subst_comp in q. rewrite hyperdoctrine_pr1_subst in q. rewrite var_tm_subst in q. rewrite hyperdoctrine_pair_pr1 in q. rewrite !tm_subst_var in q. pose proof (weaken_to_empty q : Δ ⊢ _) as q'. clear q. rename q' into q. exact (impl_elim p q). 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.PartialEqRels.PERs.