English
The product construction is functorial: given morphisms f: α ⟹ β and g: α' ⟹ β', there is a map between α ⊗ α' and β ⊗ β' that acts componentwise using f, g on the heads and tails of the vectors.
Русский
Конструкция произведения функциональна: для отображений f и g существует отображение между α ⊗ α' и β ⊗ β', действующее компонентно через f и g.
LaTeX
$$$\\mathrm{map} : (\\alpha \\Rightarrow \\beta) \\to (\\alpha' \\Rightarrow \\beta') \\to (\\alpha \\otimes \\alpha') \\Rightarrow (\\beta \\otimes \\beta').$$$
Lean4
/-- `prod` is functorial -/
protected def map : ∀ {n} {α α' β β' : TypeVec.{u} n}, α ⟹ β → α' ⟹ β' → α ⊗ α' ⟹ β ⊗ β'
| succ _, α, α', β, β', x, y, Fin2.fs _, a =>
@prod.map _ (drop α) (drop α') (drop β) (drop β') (dropFun x) (dropFun y) _ a
| succ _, _, _, _, _, x, y, Fin2.fz, a => (x _ a.1, y _ a.2)
