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