English
If f, g, h, f', g', h' satisfy a distributive compatibility across four layers, then image₂ f (image₂ g s t) (image₂ h u v) equals image₂ f' (image₂ g' s u) (image₂ h' t v).
Русский
Если функции образа совместимы по четырем слоям так, чтобы сохранять диспозицию, тогда образ₂ с двумя слоями равен обобщенному образу₂.
LaTeX
$$$\forall a b c d,\f (g a b) (h c d) = f' (g' a c) (h' b d) \Rightarrow \mathrm{image}_2 f (\mathrm{image}_2 g s t) (\mathrm{image}_2 h u v) = \mathrm{image}_2 f' (\mathrm{image}_2 g' s u) (\mathrm{image}_2 h' t v)$$$
Lean4
theorem image₂_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image₂ f s t = image₂ g t s :=
(image₂_swap _ _ _).trans <| by simp_rw [h_comm]
