Proposition hyperdoctrine_subst_eq {H : first_order_hyperdoctrine} {Γ Γ' B : ty H} {Δ : form _} {s₁ s₂ : tm Γ Γ'} (p : Δ ⊢ s₁ ≡ s₂) (t : tm Γ' B) : Δ ⊢ t [ s₁ ]tm ≡ t [ s₂ ]tm. Proof. pose (φ := t [ s₁ [ π₁ (tm_var _) ]tm ]tm ≡ t [ π₂ (tm_var _) ]tm). assert (Δ ⊢ φ [⟨ tm_var Γ, s₁ ⟩]) as q. { unfold φ. rewrite equal_subst. rewrite !tm_subst_comp. rewrite hyperdoctrine_pr1_subst. rewrite hyperdoctrine_pr2_subst. rewrite var_tm_subst. rewrite hyperdoctrine_pair_pr1. rewrite hyperdoctrine_pair_pr2. rewrite tm_subst_var. apply hyperdoctrine_refl. } pose (r := hyperdoctrine_eq_elim φ p q). unfold φ in r. rewrite equal_subst in r. rewrite !tm_subst_comp in r. rewrite hyperdoctrine_pr1_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 tm_subst_var in r. exact r. Qed.
Require Import UniMath.Foundations.All. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation.