Proposition hyperdoctrine_eq_pair_right {H : first_order_hyperdoctrine} {Γ A B : ty H} {Δ : form Γ} (s : tm Γ A) {t₁ t₂ : tm Γ B} (p : Δ ⊢ t₁ ≡ t₂) : Δ ⊢ ⟨ s , t₁ ⟩ ≡ ⟨ s , t₂ ⟩. Proof. pose (φ := (⟨ s [ π₁ (tm_var _) ]tm , t₁ [ π₁ (tm_var _) ]tm ⟩ ≡ ⟨ s [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩) : form (Γ ×h B)). assert (Δ ⊢ φ [⟨ tm_var Γ , t₁ ⟩]) as r. { unfold φ. rewrite equal_subst. rewrite !hyperdoctrine_pair_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 (hyperdoctrine_eq_elim φ p r) as r'. unfold φ in r'. rewrite equal_subst in r'. rewrite !hyperdoctrine_pair_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.