Спочатку джерела (в хронологічному для мене порядку) які заставили мене копати.
deni-ok: (f .) . (. h) = (. h) . (f .)Wikipedia: Hom-functorCrash Monad Tutorial: Natural Transformation Я довго думав над комутативною діаграмою намагаючись зрозуміти її суть доки не розклав все по деталям.
Маємо:
Пара функторів F,G: X → Y
Морфізм у категорії X f: a → b
Natural transformation φ: F → G
Розглянемо функтор F:
F(a): aY - об’єкт категорії Y
F(b): bY - об’єкт категорії Y
F(f): fY: aY → bY - морфізм (стрілка) в категорії Y
Розглянемо функтор G:
G(a): aY' - об’єкт категорії Y
G(b): bY' - об’єкт категорії Y
G(f): fY': aY' → bY' - морфізм (стрілка) в категорії Y
Розглянемо пару морфізмів:
φ(a): F(a) -> G(a): aY → aY' - морфізм (стрілка) в категорії Y
φ(b): F(b) -> G(b): bY → bY' - морфізм (стрілка) в категорії Y
Власне, перетворення:
G(f) ∘ φ(a) = φ(b) ∘ F(f)
Розкладемо його по морфізмам і об’єктам:
(aY' → bY') ∘ (aY → aY') = (bY → bY') ∘ (aY → bY)
Оскільки A ∘ B = A(B) (композиція) маємо такі послідовності:
aY → aY' → bY'
aY → bY → bY'
Результати співпадають, значить G(f) ∘ φ(a) = φ(b) ∘ F(f) - істина.
Залишилось осмилити оце:
point-free style на стероїдах (і наступні коментарі від nikov).