Proposition from_eq_partial_setoid_morphism_b {φ₁ φ₂ : partial_setoid_morphism} (p : φ₁ = φ₂) {Γ : ty H} {Δ : form Γ} {t₁ : tm Γ X} {t₂ : tm Γ Y} (q : Δ ⊢ φ₂ [ ⟨ t₁ , t₂ ⟩ ]) : Δ ⊢ φ₁ [ ⟨ t₁ , t₂ ⟩ ]. Proof. refine (hyperdoctrine_cut q _). use hyperdoctrine_proof_subst. exact (hyperdoctrine_formula_eq_b (maponpaths pr1 p)). 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.