Definition per (X : ty H) : UU := ∑ (e : per_data X), per_axioms e. Coercion per_to_data {X : ty H} (e : per X) : form (X ×h X). Proof. exact (pr1 e). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.