Proposition hyperdoctrine_eq_transportf {H : first_order_hyperdoctrine} {Γ A : ty H} {Δ : form Γ} {t₁ t₂ : tm Γ A} (φ : form A) (p : Δ ⊢ t₁ ≡ t₂) (q : Δ ⊢ φ [ t₁ ]) : Δ ⊢ φ [ t₂ ]. Proof. assert (Δ ⊢ t₁ ≡ t₂ ∧ φ [ t₁ ]) as r. { exact (conj_intro p q). } refine (hyperdoctrine_cut r _). pose (hyperdoctrine_eq_elim (φ [ π₂ (tm_var _) ]) (weaken_left (hyperdoctrine_hyp _) _) (weaken_right (hyperdoctrine_hyp _) (t₁ ≡ t₂))) as h. rewrite !hyperdoctrine_comp_subst in h. rewrite !hyperdoctrine_pr2_subst in h. rewrite !var_tm_subst in h. rewrite !hyperdoctrine_pair_pr2 in h. exact h. 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.