English
Let f0: α0 ⟹ α1 and f1: α1 ⟹ α2 be morphisms between TypeVec objects of length n+1. Then the last-coordinate functor preserves composition: lastFun (f1 ∘ f0) = (lastFun f1) ∘ (lastFun f0).
Русский
Пусть f0: α0 ⟹ α1 и f1: α1 ⟹ α2 — морфизмы между объектами TypeVec длины n+1. Тогда отображение по последнему компоненту сохраняет композицию: lastFun (f1 ∘ f0) = lastFun f1 ∘ lastFun f0.
LaTeX
$$$$\\operatorname{lastFun}(f_1 \\circ f_0) = \\operatorname{lastFun}(f_1) \\circ \\operatorname{lastFun}(f_0).$$$$
Lean4
@[simp]
theorem lastFun_comp {α₀ α₁ α₂ : TypeVec (n + 1)} (f₀ : α₀ ⟹ α₁) (f₁ : α₁ ⟹ α₂) :
lastFun (f₁ ⊚ f₀) = lastFun f₁ ∘ lastFun f₀ :=
rfl
