English
Let F, G : C ⥤ FintypeCat be functors and σ : F ⟶ G a natural transformation. For any morphism f : X ⟶ Y in C and any element x ∈ F.obj X, the naturality condition is that σ.app Y (F.map f x) = G.map f (σ.app X x).
Русский
Пусть F, G : C ⥤ FintypeCat — функторы и σ : F ⟶ G — естественное преобразование. Для любого морфизма f : X ⟶ Y в C и любого элемента x ∈ F.obj X выполняется условие естественности: σ.app Y (F.map f x) = G.map f (σ.app X x).
LaTeX
$$$ \forall F,G : C \to \mathrm{FintypeCat}, \; \sigma : F \Rightarrow G, \; f : X \to Y, \; x \in F(X): \quad \sigma_Y(F.map f\, x) = G.map f\, (\sigma_X x). $$$
Lean4
theorem naturality (σ : F ⟶ G) (f : X ⟶ Y) (x : F.obj X) : σ.app Y (F.map f x) = G.map f (σ.app X x) :=
congr_fun (σ.naturality f) x
