> Here you're making the argument that things are not so simple with Haskell.

Well, just different I guess. I'll go into this below.

> I still wonder though to what extent it is true within pure category theory. At least for the basic stuff I've going through, almost all the weight of the matter has been concentrated in the definitions rather than the proofs. Does this trend continue into the more advanced realms of category theory?

There are complicated proofs in CT. I am not sure how deep your course is going to dive.

-------------------------------------------------------

In Haskell, the functor \\(h^A\\) corresponds to `(->) a`. We call `(->) a` the _reader monad_.

Since Haskell doesn't have sets, we can't really talk about \\(Nat(F,G)\\). Instead, we use a _type_ for natural transformations:


{-# LANGUAGE RankNTypes, TypeOperators #-}

infixr 0 ~>
type f ~> g = forall x. f x -> g x

Note: In conventional category theory we demand a natural transformation \\(\eta\\) obey a law, appropriately called _naturality_. The law asserts that for any natural transformation \\(\eta : F \to G\\) we have that for all \\(f : X \to Y\\) that

\\[
\eta_Y \circ F f \cong G f \circ \eta_X
\\]

Haskell can't enforce this, so we just assume it. Languages with more powerful type systems like Coq's and Idris' can enforce this rule.

You _can_ write \\(\eta_X\\) in Haskell as `eta @X` by turning a language extension. Just put `{-# LANGUAGE TypeApplications #-}` at the top of your file.

-------------------------------------------------------

Anyhow, the Yoneda lemma \\(Nat(h^A, F) \cong F A\\) in Haskell would be written as

`((->) a ~> f) ≅ f a`

Or in other words

`(forall b. (a -> b) -> f b) ≅ f a`

The proof of the Yoneda lemma corresponds to writing two functions:


liftYoneda :: Functor f => f a -> ((->) a ~> f)
liftYoneda = ...

lowerYoneda :: ((->) a ~> f) -> f a
lowerYoneda = ...


Then show that `lowerYoneda . liftYoneda = id` and `liftYoneda . lowerYoneda = id`.

Feel free to give it a try, or if you prefer I can show you the answers here.

But I maintain the chief take away is this: **In Haskell, types take the place of sets.** It makes things more confusing I'm afraid :(