English
A generalized associativity for map₂: if f, g, f', g' satisfy a compatibility condition, then map₂ f (map₂ g a b) c equals map₂ f' a (map₂ g' b c).
Русский
Обобщённая ассоциативность для map₂: если функции согласованы, то map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c).
LaTeX
$$$ \forall a\, b\, c, \; f (g a b) c = f' a (g' b c) \Rightarrow \mathrm{map}_2 f (\mathrm{map}_2 g a b) c = \mathrm{map}_2 f' a (\mathrm{map}_2 g' b c) $$$
Lean4
theorem map₂_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
(h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) : map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c) := by grind
