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