Definition per_symm_axiom {X : ty H} (e : per_data X) : UU := let x := π₂ (π₁ (tm_var _)) : tm ((𝟙 ×h X) ×h X) X in let y := π₂ (tm_var _) : tm ((𝟙 ×h X) ×h X) X in ⊤ ⊢ (∀h ∀h (e [ ⟨ x , y ⟩ ] ⇒ e [ ⟨ y , x ⟩ ])).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.