Не совсем понимаю `F (1A) = 1F (A) ∀ A ∈ C1 ' как закон функтора

Я читаю эту статью о категории и Функторе в scala: https://hseeberger.wordpress.com/2010/11/25/introduction-to-category-theory-in-scala/

В этой части:

Для сохранения структуры категорий это отображение должно сохранять карты идентичности и композиции. Более формально:

F (1 A) = 1F (A) ∀ A ∈ C1

F (g ο f) = F (g) ο F (f) ∀ f: A → B, g: B → C, где A, B, C ∈ C1

I не могу хорошо понять о: F(1 A) = 1F (A)

Почему правая часть равна 1 F (A) , а не F(A)?

Я вижу в других статьях закон тождества для функтора: 

fa.map(a => a) == fa

Который не относится к 1 F (A)

2 2
scala functional-programming functor

2 ответа:

Я думаю, что вы путаетесь в том, что представляет собой нотация.

1A представляет собой стрелку идентичности, которая является просто стрелкой / отображением от объекта A в категории к себе, т. е. A -> A.

Аналогично, 1F (A) представляет собой тождественный функтор, который является просто стрелкой от функтора F(A) к самому себе, т. е. F(A) -> F(A).

Поэтому стрелка 1 F (A) не совпадает с функтором F (A), и поэтому было бы неверно говорить, что 1F (A) = F(A) как ты и предлагаешь.

Чтобы ответить на ваш вопрос, почему F (1 A) = 1F (A) , рассмотрим следующее В свете приведенного выше объяснения:

F (1 A ) = F(f : A - > A) = F (f) : F (A) - > F (A) = 1F (A)

Кроме того, теперь, когда мы прояснили значение обозначения, фрагмент кода согласуется с определением функтора: 

fa.map(a => a) == fa

fa является функтором, и карта использует функцию идентификации, чтобы сопоставить каждый элемент функтора самому себе. Этот воспроизводит функтор, эквивалентный исходному функтору fa, и поэтому отображение может быть представлено как 1 F(A) на языке теории категорий.

Таким образом, вы можете видеть, что в теории категорий есть понятие стрелки и объекта, которое вы должны уметь различать и понимать, глядя на обозначения. Я настоятельно рекомендую прочитать первую главутеории категорий Стива Аводи , Если вы действительно заинтересованы в этом предмете.
6

Если A-объект в исходной категории, то F(A) - соответствующий объект в новой категории. Если в исходной категории имеется стрелка A->B, то в новой категории должна быть соответствующая стрелка F(A)->F(B). Поскольку 1 A-это просто стрелка A->A, это означает, что должна быть также стрелка F(A) - >F(A), которая была бы записана 1 F(A). Более компактно, F (1A) = 1F (A) .

3