Proposition per_subobject_mor {X Y : partial_setoid H} {φ : partial_setoid_morphism X Y} {ψ₁ : per_subobject X} {ψ₂ : per_subobject Y} (p : per_subobject_mor_law φ ψ₁ ψ₂) {Γ : ty H} {Δ : form Γ} {x : tm Γ X} {y : tm Γ Y} (q₁ : Δ ⊢ φ [ ⟨ x , y ⟩ ]) (q₂ : Δ ⊢ ψ₁ [ x ]) : Δ ⊢ ψ₂ [ y ]. Proof. use (impl_elim q₂). use (impl_elim q₁). pose proof (hyperdoctrine_proof_subst (!! : tm Γ 𝟙) p) as r. cbn in r. rewrite truth_subst in r. rewrite !forall_subst in r. rewrite !impl_subst in r. rewrite !hyperdoctrine_comp_subst 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 !hyperdoctrine_pair_subst 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 hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite hyperdoctrine_pr2_subst in r. rewrite !var_tm_subst in r. rewrite hyperdoctrine_pair_pr2 in r. pose proof (r' := forall_elim r x) ; clear r. rewrite forall_subst in r'. rewrite !impl_subst in r'. rewrite !hyperdoctrine_comp_subst 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 !hyperdoctrine_pair_subst 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 hyperdoctrine_pr2_subst in r'. rewrite !var_tm_subst in r'. rewrite hyperdoctrine_pair_pr2 in r'. pose proof (r'' := forall_elim r' y) ; clear r'. rewrite !impl_subst in r''. rewrite !hyperdoctrine_comp_subst in r''. rewrite !hyperdoctrine_pr2_subst in r''. rewrite !var_tm_subst in r''. rewrite hyperdoctrine_pair_pr2 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''. refine (hyperdoctrine_cut _ r''). 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.