Proposition eq_per_axioms (X : ty H) : per_axioms (π₁ (tm_var (X ×h X)) ≡ π₂ (tm_var (X ×h X))). Proof. split. - unfold per_symm_axiom. pose (T := X). pose (x := π₂ (π₁ (tm_var ((𝟙 ×h T) ×h T)))). pose (y := π₂ (tm_var ((𝟙 ×h T) ×h T))). unfold T in *. fold x y. simplify. use forall_intro. use forall_intro. use impl_intro. use weaken_right. use hyperdoctrine_eq_sym. apply hyperdoctrine_hyp. - unfold per_trans_axiom. pose (T := X). pose (x := π₂ (π₁ (π₁ (tm_var (((𝟙 ×h T) ×h T) ×h T))))). pose (y := π₂ (π₁ (tm_var (((𝟙 ×h T) ×h T) ×h T)))). pose (z := π₂ (tm_var (((𝟙 ×h T) ×h T) ×h T))). unfold T in *. fold x y z. simplify. use forall_intro. use forall_intro. use forall_intro. use impl_intro. use impl_intro. simplify. use hyperdoctrine_eq_trans. + exact y. + use weaken_left. use weaken_right. apply hyperdoctrine_hyp. + use weaken_right. apply hyperdoctrine_hyp. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.