English
A related construction toSubtype' reindexes a relation p on α × α into a vector of subtypes via the product and repeats.
Русский
Связная конструкция toSubtype' перераспределяет отношение на пары элементов α × α в вектор подтипов через произведение и повторения.
LaTeX
$$$\\mathrm{toSubtype}' : (p : (α \\otimes α) \\Rightarrow \\mathrm{repeat}\\; n\\; \\mathrm{Prop}) \\Rightarrow (\\mathrm{TypeVec}\\, n \\Rightarrow \\mathrm{Subtype_} p)$$$
Lean4
/-- arrow that rearranges the type of `Subtype_` to turn a vector of subtypes
into a subtype of vector -/
def ofSubtype {n} {α : TypeVec.{u} n} (p : α ⟹ «repeat» n Prop) :
Subtype_ p ⟹ fun i : Fin2 n => { x // ofRepeat <| p i x }
| Fin2.fs i, x => ofSubtype _ i x
| Fin2.fz, x => x
