English
Uniformity is defined as a property asserting that all coordinate-wise ranges of equivalent representations coincide.
Русский
Однородность определяется как свойство, утверждающее совпадение диапазонов по координатам для эквивалентных представлений.
LaTeX
$$$$ \\mathrm{IsUniform} :\\; \\forall a,a',f,f',\\ \\mathrm{abs}\\langle a,f\\rangle = \\mathrm{abs}\\langle a',f'\\rangle \\Rightarrow \\forall i,\\ f(i)'' univ = f'(i)'' univ. $$$$
Lean4
/-- A qpf is said to be uniform if every polynomial functor
representing a single value all have the same range. -/
def IsUniform : Prop :=
∀ ⦃α : TypeVec n⦄ (a a' : q.P.A) (f : q.P.B a ⟹ α) (f' : q.P.B a' ⟹ α),
abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ i, f i '' univ = f' i '' univ
