Not quite understand `F(1A) = 1F(A) ∀ A ∈ C1` as the Functor law

Question

I'm reading this article about Category and Functor in scala: https://hseeberger.wordpress.com/2010/11/25/introduction-to-category-theory-in-scala/

In this part:

In order to preserve the category structure this mapping must preserve the identity maps and the compositions. More formally:

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

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

I can't understand well about: F(1_A) = 1_F(A)

Why the right part is 1_F(A) rather than F(A)?

I see in other articles, the identity law for Functor is:

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

Which doesn't relate to 1_F(A)

Answer 1

I think you are confused about what the notation represents.

1_A represents the identity arrow which is just an arrow/mapping from the object A in the category to itself i.e. A -> A.

Similarly, 1_F(A) represents the identity functor which is just an arrow from the functor F(A) to itself ie F(A) -> F(A).

Therefore, the arrow 1_F(A) is not the same as the functor F(A) and so it would be wrong to say that 1_F(A) = F(A) as you suggest.

To answer your question why F(1_A) = 1_F(A), consider the following in light of the above explanation:

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

Also now that we have cleared up the meaning of the notation, the code snippet is consistent with the functor definition:

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

fa is a functor and the map is using the identity function to map every element of the functor to itself. This reproduces a functor which is equivalent to the original functor fa and so the map can be represented as 1_F(A) in the language of category theory.

So you can see there is a concept of an arrow and an object in Category Theory which you must be able to distinguish and understand when looking at the notation. I highly recommend reading the first chapter of Steve Awodey's Category Theory if you are really interested in this subject.

Answer 2

If A is an object in the original category, then F(A) is the corresponding object in the new category. If there is an arrow A->B in the original category, there must be a corresponding arrow F(A)->F(B) in the new category. Since 1_A is just an arrow A->A, this means there must be an arrow F(A)->F(A) as well, which would be written 1_F(A). More compactly, F(1_A) = 1_F(A).