Proposition hyperdoctrine_eq_elim {H : first_order_hyperdoctrine} {Γ A : ty H} {Δ : form Γ} (φ : form (Γ ×h A)) {t₁ t₂ : tm Γ A} (p : Δ ⊢ t₁ ≡ t₂) (q : Δ ⊢ φ [ ⟨ tm_var _ , t₁ ⟩ ]) : Δ ⊢ φ [ ⟨ tm_var _ , t₂ ⟩ ]. Proof. pose (φ [ ⟨ π₁ (tm_var _) , (π₁ (tm_var _)) [ π₂ (tm_var _) ]tm ⟩ ] ⇒ φ [ ⟨ π₁ (tm_var _) , (π₂ (tm_var _)) [ π₂ (tm_var _) ]tm ⟩ ]) as ψ. assert (⊤ ⊢ ψ [⟨ π₁ (tm_var (Γ ×h A)), Δ_{ A } [ π₂ (tm_var (Γ ×h A)) ]tm ⟩]) as r. { unfold ψ. rewrite impl_subst. rewrite !hyperdoctrine_comp_subst. rewrite !hyperdoctrine_pair_subst. rewrite !tm_subst_comp. rewrite hyperdoctrine_pair_comp_pr1. rewrite hyperdoctrine_pair_comp_pr2. rewrite <- !tm_subst_comp. unfold hyperdoctrine_diag. rewrite hyperdoctrine_pair_comp_pr1. rewrite hyperdoctrine_pair_comp_pr2. rewrite !var_tm_subst. apply impl_id. } pose proof (hyperdoctrine_eq_elim_help_con ψ r t₁ t₂) as r'. unfold ψ in r'. rewrite impl_subst in r'. rewrite !hyperdoctrine_comp_subst in r'. rewrite !hyperdoctrine_pair_subst in r'. rewrite !tm_subst_comp in r'. rewrite hyperdoctrine_pair_comp_pr1 in r'. rewrite hyperdoctrine_pair_comp_pr2 in r'. rewrite hyperdoctrine_pair_comp_pr1 in r'. rewrite hyperdoctrine_pair_comp_pr2 in r'. use (impl_elim q). use (hyperdoctrine_cut p). 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.