Definition eq_per (X : ty H) : per X. Proof. use make_per. - exact (π₁ (tm_var _) ≡ π₂ (tm_var _)). - exact (eq_per_axioms X). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.