Definition prod_per_data : form ((X ×h Y) ×h X ×h Y) := let x := π₁ (tm_var _) : tm ((X ×h Y) ×h X ×h Y) (X ×h Y) in let y := π₂ (tm_var _) : tm ((X ×h Y) ×h X ×h Y) (X ×h Y) in π₁ x ~ π₁ y ∧ π₂ x ~ π₂ y.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine. Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.