52700.fb2
анаморфизм отображают объекты в стрелки. По типу функций fold и unfold мы можем сделать вывод, что
объектами в нашей категории будут стрелки вида
f a -> a
или для свёрток:
a -> f a
А стрелками будут обычные функции одного аргумента. Теперь дадим более формальное определение.
Эндофунктор F : A → A определяет стрелки α : F A → A, которые называется F - алгебрами. Стрелку
h : A → B называют F - гомоморфизмом, если следующая диаграмма коммутирует:
F A
α
A
F h
h
F B
B
β
Или можно сказать по другому, для F -алгебр α : F A → A и β : F B → B выполняется:
F h ; β = α ; h
Это свойство совпадает со свойством естественного преобразования только вместо одного из функторов
мы подставили тождественный функтор I. Определим категорию Alg( F ), для категории A и эндофунктора
F : A → A
• Объектами являются F -алгебры F A → A, где A – объект категории A
• Два объекта α : F A → A и β : F B → B соединяет F -гомоморфизм h : A → B. Это такая стрелка из
A, для которой выполняется:
F h ; β = α ; h
• Композиция и тождественная стрелка взяты из категории A.
Если в этой категории есть начальный объект inF : F T → T , то определён катаморфизм, который
переводит объекты F A → A в стрелки T → A. Причём следующая диаграмма коммутирует:
in
F T
F
T
F ( | α |)
( | α |)
F A
A
α
Этот катаморфизм и будет функцией свёртки для рекурсивного типа . Понятие Alg( F ) можно перевернуть
и получить категорию CoAlg( F ).
244 | Глава 16: Категориальные типы
• Объектами являются F -коалгебры A → F A, где A – объект категории A
• Два объекта α : F A → A и β : F B → B соединяет F -когомоморфизм h : A → B. Это такая стрелка
из A, для которой выполняется:
h ; α = β ; F h
• Композиция и тождественная стрелка взяты из категории A.
Если в этой категории есть конечный объект, его называют outF : T → F T , то определён анаморфизм,
который переводит объекты A → F A в стрелки A → T .
Причём следующая диаграмма коммутирует:
in