Proposition per_subobject_eq {X : partial_setoid H} (φ : per_subobject X) {Γ : ty H} {Δ : form Γ} {x y : tm Γ X} (p₁ : Δ ⊢ x ~ y) (p₂ : Δ ⊢ φ [ x ]) : Δ ⊢ φ [ y ]. Proof. use (impl_elim p₂). use (impl_elim p₁). pose proof (hyperdoctrine_proof_subst (!! : tm Γ 𝟙) (pr22 φ)) as q. cbn in q. rewrite truth_subst in q. rewrite !forall_subst in q. rewrite !impl_subst in q. rewrite !partial_setoid_subst in q. rewrite !hyperdoctrine_comp_subst in q. 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. rewrite hyperdoctrine_pair_subst in q. rewrite hyperdoctrine_pair_pr2 in q. rewrite hyperdoctrine_pr2_subst in q. rewrite !var_tm_subst in q. pose proof (q' := forall_elim q x) ; clear q. rewrite forall_subst in q'. rewrite !impl_subst in q'. rewrite !partial_setoid_subst in q'. rewrite !hyperdoctrine_comp_subst in q'. 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'. rewrite hyperdoctrine_pair_subst in q'. rewrite hyperdoctrine_pair_pr2 in q'. pose proof (q'' := forall_elim q' y) ; clear q'. rewrite !impl_subst in q''. rewrite !partial_setoid_subst in q''. rewrite !hyperdoctrine_comp_subst in q''. rewrite !tm_subst_comp in q''. rewrite !hyperdoctrine_pr1_subst in q''. rewrite !hyperdoctrine_pr2_subst in q''. rewrite !var_tm_subst in q''. rewrite hyperdoctrine_pair_pr1 in q''. rewrite hyperdoctrine_pair_pr2 in q''. rewrite !tm_subst_var in q''. refine (hyperdoctrine_cut _ q''). apply truth_intro. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms. Require Import UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory.