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

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

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

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

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

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

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

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

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

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

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

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