English
For every multivariate functor F and every x ∈ F α, applying the identity on all coordinates leaves x unchanged: map_id(x) = x.
Русский
Для каждого многоизмеренного функторa F и каждого x ∈ F α применение тождественного отображения к каждой координате не меняет x: map_id(x) = x.
LaTeX
$$$$F.map(\\mathrm{id})\\,x = x.$$$$
Lean4
protected theorem id_map {α : TypeVec n} (x : F α) : TypeVec.id <$$> x = x :=
by
rw [← abs_repr x, ← abs_map]
rfl