English
Let f be a morphism between the index tuples α and β for a multivariate functor, and let x be an element of the composed functor comp P Q applied to α. Then applying f inside x and then taking the composed-get is equal to first taking the composed-get of x and then applying f componentwise to its result.
Русский
Пусть f — морфизм между кортежами индексов α и β для мультфункторной конструкции, и пусть x ∈ comp P Q α. Тогда применение f внутри x и затем извлечение результата через comp.get совпадает с сначала извлечением comp.get из x, а затем по компонентам применением f.
LaTeX
$$$\\operatorname{comp.get}\\bigl( f \\<$$> x \\bigr) \\;=\\; \\bigl( \\lambda i (y : Q\,i\,α),\\; f \\<$$> y \\bigr) \\<$$> \\operatorname{comp.get} x$$$
Lean4
theorem get_map (f : α ⟹ β) (x : comp P Q α) : comp.get (f <$$> x) = (fun i (x : Q i α) => f <$$> x) <$$> comp.get x :=
by rfl
