Icelandjack · April 8, 2024 11:08 · May 12, 2020 · May 12, 2020 · Nov 27, 2018 · Nov 27, 2018
diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -10,7 +10,7 @@ I am not out to motivate it, but we will explore Yoneda at the level of terms an
 
 > "[Yoneda lemma], arguably the most important result in category theory."
 > 
-> [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
+> [*Emily Riehl*](http://www.math.jhu.edu/~eriehl/context.pdf)
 
 (congratulations on not running away after "Yoneda lemma" or "category theory", what are you on)
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -111,9 +111,26 @@ Interesting. Is this what you expected?
 
 Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole) (bonus points if you physically act this out every time you use Yoneda).
 
-Imagine we have a magical Yoneda crossbow (no I don't know archercy, so this will be a funky). I think of `Yoneda [] Int` (Yoneda form of `[Int]`) like a cocked crossbow: we have "pulled" the `Int` out of it we get a very tightly-strung `(Int -> x)`, leaving a list of holes `[x]`.
+Imagine we have a magical Yoneda crossbow (I don't know archery). I think of `Yoneda [] Int` (Yoneda form of `[Int]`) like a cocked crossbow: we have "pulled" the `Int` out of it, it's now a tightly-strung arrow `Int -> x` waiting to fire the values into `[x]`.
+
+In effect, beause of the polymorphism, there are two arguments. The type `x` (invisible) and the arrow `Int -> x` (visible).
+
+The choice of arrow is important but the type is no less important, instanting the type to `@String` firing the arrow `show :: Int -> String` gives a list of strings:
+
+```haskell
+  yoList @String show :: [String]
+= ["1", "2", "3"]
+```
+
+Choosing `@Int` as the type and `\a -> 2 * a * a` as the arrow yields yet another expression
+
+```haskell
+  yoList @Int \a -> 2 * a * a :: [Int]
+= [2, 8, 18]
+```
+
+But something special happens when we fire at `@Int` with the arrow `id :: Int -> Int`. We get back the original list.
 
-To fire we load it with a *1)* type `@Int` and *2)* function (arrow) `id :: Int -> Int`
 1. Remember that `yoList :: forall x. (Int -> x) -> [x]` actually takes `x` as an invisible argument. GHC usually solves it with unifiation but our first step is to instantiate `x` with a type: with crucial use of the `yoList` polymorphism we pick `Int` using [visible type applications](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application)
 
     ```haskell

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -17,7 +17,7 @@ I am not out to motivate it, but we will explore Yoneda at the level of terms an
 ## Yoneda; Term level
 
 ```haskell
-[1, 2, 3]
+[1..3]
 ```
 
 Every list can be expressed as a (higher-order) function by viewing it through our Yoneda-tinted glasses 🕶:
@@ -28,23 +28,23 @@ Every list can be expressed as a (higher-order) function by viewing it through o
 
 It's like the function `f` grabs a hold of each element. I'll call it `post` because it does "postprocessing".
 
-The Yoneda lemma states that `[1, 2, 3]` and `\f -> [f 1, f 2, f 3]` are equivalent! (naturally isomorphic)
+The Yoneda lemma states that `[1..3]` and `\f -> [f 1, f 2, f 3]` are equivalent! (naturally isomorphic)
 
 How do we go back? We pass it the identity function:
 
 ```haskell
   (\post -> [post 1, post 2, post 3]) id
 = [id 1, id 2, id 3]
-= [1, 2, 3]
+= [1..3]
 ```
 
-The Yoneda form of `[1, 2, 3]` can be understood without `(f)map` but it is really `map` partially applied to its second argument:
+The Yoneda form of `[1..3]` can be understood without `(f)map` but it is really `map` partially applied to its second argument:
 
 ```haskell
   \post -> [post 1, post 2, post 3]
-= \post -> map post [1, 2, 3]
-= flip map [1, 2, 3]
-= (<$> [1, 2, 3])
+= \post -> map post [1..3]
+= flip map [1..3]
+= (<$> [1..3])
 ```
 
 This works for any `Functor`, the Yoneda forms of `Just True` and `Nothing` are
@@ -97,7 +97,7 @@ Our first example used `Functor []`
 
 ```haskell
 list :: [Int]
-list = [1, 2, 3]
+list = [1..3]
 ```
 
 So what is the type of the Yoneda form? (switching back from `post` to `f`)
@@ -236,7 +236,7 @@ so with [`RankNTypes`](https://downloads.haskell.org/~ghc/latest/docs/html/users
 >>
 >> :t (\f -> [f 1, f 2, f 3]) :: Yoneda [] Int
 .. :: (Int -> xx) -> [xx]
->> :t (<$> [1,2,3]) :: Yoneda [] Int
+>> :t (<$> [1..3]) :: Yoneda [] Int
 .. :: (Int -> xx) -> [xx]
 ```
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -111,12 +111,10 @@ Interesting. Is this what you expected?
 
 Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole) (bonus points if you physically act this out every time you use Yoneda).
 
-I think about this like cocking a crossbow (no I don't know archercy, so this will be a funky mythological bow):
+Imagine we have a magical Yoneda crossbow (no I don't know archercy, so this will be a funky). I think of `Yoneda [] Int` (Yoneda form of `[Int]`) like a cocked crossbow: we have "pulled" the `Int` out of it we get a very tightly-strung `(Int -> x)`, leaving a list of holes `[x]`.
 
-The Yoneda form of `[Int]` is like a loaded crossbow: we have "pulled" the `Int` out of it `(Int -> x)`, leaving a list of holes `[x]`.
-
-To fire we take two steps:
-1. Remember that `yoList` actually takes `x` as an invisible argument: `forall x. (Int -> x) -> [x]`. This means our first step is to instantiate `x` with a type: with crucial use of the polymorphism of `yoList` we pick `Int` using [visible type applications](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application)
+To fire we load it with a *1)* type `@Int` and *2)* function (arrow) `id :: Int -> Int`
+1. Remember that `yoList :: forall x. (Int -> x) -> [x]` actually takes `x` as an invisible argument. GHC usually solves it with unifiation but our first step is to instantiate `x` with a type: with crucial use of the `yoList` polymorphism we pick `Int` using [visible type applications](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application)
 
     ```haskell
     yoList @Int :: (Int -> Int) -> [Int]

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -12,7 +12,7 @@ I am not out to motivate it, but we will explore Yoneda at the level of terms an
 > 
 > [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
 
-(congratulations on not running away after "Yoneda lemma" and "category theory", what are you on)
+(congratulations on not running away after "Yoneda lemma" or "category theory", what are you on)
 
 ## Yoneda; Term level
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -1,5 +1,6 @@
 (previous [Yoneda blog](https://gist.github.com/Icelandjack/aecf49b75afcfcee9ead29d27cc234d5))
 ([reddit](https://www.reddit.com/r/haskell/comments/a0nyjj/yoneda_intuition_from_humble_beginnings/))
+([twitter](https://twitter.com/Iceland_jack/status/1067173831708688384))
 
 # Yoneda Intuition from Humble Beginnings
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -11,7 +11,7 @@ I am not out to motivate it, but we will explore Yoneda at the level of terms an
 > 
 > [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
 
-(congratulation on not running away after "Yoneda lemma" and "category theory", what are you on)
+(congratulations on not running away after "Yoneda lemma" and "category theory", what are you on)
 
 ## Yoneda; Term level
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -11,6 +11,8 @@ I am not out to motivate it, but we will explore Yoneda at the level of terms an
 > 
 > [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
 
+(congratulation on not running away after "Yoneda lemma" and "category theory", what are you on)
+
 ## Yoneda; Term level
 
 ```haskell

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -235,6 +235,8 @@ so with [`RankNTypes`](https://downloads.haskell.org/~ghc/latest/docs/html/users
 >>
 >> :t (\f -> [f 1, f 2, f 3]) :: Yoneda [] Int
 .. :: (Int -> xx) -> [xx]
+>> :t (<$> [1,2,3]) :: Yoneda [] Int
+.. :: (Int -> xx) -> [xx]
 ```
 
 and now we 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -227,7 +227,7 @@ yoConstAbc      :: forall a x. (a      -> x) -> Const String x
 (<$> show @Int) :: forall   x. (String -> x) -> (Int -> x)
 ```
 
-so with [`RankNTypes`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-RankNTypes) we can `Yoneda` a name (I use a type synonym for simplicity, you will want to use a `newtype` like [`Data.Functor.Yoneda`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html#t:Yoneda))
+so with [`RankNTypes`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-RankNTypes) we can give Yoneda a name (I use a type synonym for simplicity, you will want to use a `newtype` like [`Data.Functor.Yoneda`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html#t:Yoneda))
 
 ```
 >> :set -XRankNTypes

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -1,4 +1,5 @@
 (previous [Yoneda blog](https://gist.github.com/Icelandjack/aecf49b75afcfcee9ead29d27cc234d5))
+([reddit](https://www.reddit.com/r/haskell/comments/a0nyjj/yoneda_intuition_from_humble_beginnings/))
 
 # Yoneda Intuition from Humble Beginnings
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -105,7 +105,7 @@ yoList f = [f 1, f 2, f 3]
 
 Interesting. Is this what you expected? 
 
-Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole) (bonus point if you physically perform this motion every time you encounter use Yoneda (covariantly)).
+Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole) (bonus points if you physically act this out every time you use Yoneda).
 
 I think about this like cocking a crossbow (no I don't know archercy, so this will be a funky mythological bow):
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -105,7 +105,7 @@ yoList f = [f 1, f 2, f 3]
 
 Interesting. Is this what you expected? 
 
-Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole).
+Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole) (bonus point if you physically perform this motion every time you encounter use Yoneda (covariantly)).
 
 I think about this like cocking a crossbow (no I don't know archercy, so this will be a funky mythological bow):
 

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -75,8 +75,16 @@ or, doing case analysis on the Boolean, we are invoking `post` on the negated Bo
 
 ```haskell
 \post -> \case    -- -XLambdaCase
-  True  -> post False
   False -> post True
+  True  -> post False
+```
+
+What happens when we pass in `id`? We get back `not`:
+
+```haskell
+\case
+  False -> True
+  True  -> False
 ```
 
 ## Yoneda; Type level

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -71,7 +71,7 @@ So we are really postcomposing `not` with our `post` function:
 \post -> fmap post not
 ```
 
-Or doing case analysis on the Boolean
+or, doing case analysis on the Boolean, we are invoking `post` on the negated Boolean.
 
 ```haskell
 \post -> \case    -- -XLambdaCase

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -64,7 +64,7 @@ Let's take the function `not` as an example, we pass the result of `not bool` to
 \post -> \bool -> post (not bool)
 ```
 
-So we are really postcomposing `post` with `not`:
+So we are really postcomposing `not` with our `post` function:
 
 ```haskell
 \post -> post . not

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -37,11 +37,10 @@ How do we go back? We pass it the identity function:
 The Yoneda form of `[1, 2, 3]` can be understood without `(f)map` but it is really `map` partially applied to its second argument:
 
 ```haskell
-\post -> [post 1, post 2, post 3]
-=
-\post -> map post [1, 2, 3]
-=
-flip map [1, 2, 3]
+  \post -> [post 1, post 2, post 3]
+= \post -> map post [1, 2, 3]
+= flip map [1, 2, 3]
+= (<$> [1, 2, 3])
 ```
 
 This works for any `Functor`, the Yoneda forms of `Just True` and `Nothing` are

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -34,7 +34,7 @@ How do we go back? We pass it the identity function:
 = [1, 2, 3]
 ```
 
-We didn't need `(f)map`. The Yoneda form of `[1, 2, 3]` can be understood without it but it is `map` partially applied to its second argument:
+The Yoneda form of `[1, 2, 3]` can be understood without `(f)map` but it is really `map` partially applied to its second argument:
 
 ```haskell
 \post -> [post 1, post 2, post 3]

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -24,7 +24,8 @@ Every list can be expressed as a (higher-order) function by viewing it through o
 
 It's like the function `f` grabs a hold of each element. I'll call it `post` because it does "postprocessing".
 
-The Yoneda lemma states that these are equivalent (naturally isomorphic)! 
+The Yoneda lemma states that `[1, 2, 3]` and `\f -> [f 1, f 2, f 3]` are equivalent! (naturally isomorphic)
+
 How do we go back? We pass it the identity function:
 
 ```haskell

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -1,3 +1,5 @@
+(previous [Yoneda blog](https://gist.github.com/Icelandjack/aecf49b75afcfcee9ead29d27cc234d5))
+
 # Yoneda Intuition from Humble Beginnings
 
 Let's explore the Yoneda lemma. You don't need to be an advanced Haskeller to understand this. In fact I claim you will understand the first section fine if you're comfortable with `map`/[`fmap`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor.html#v:fmap) and [`id`](https://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Function.html#v:id).

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -119,7 +119,7 @@ becomes
 ```haskell
 yoJust :: (Bool -> x) -> Maybe x
 yoJust f = Just (f True)
-``
+```
 
 `Nothing :: Maybe a` contains no values of type `a` but, but we can still follow the pattern:
 ```haskell

diff --git a/Yoneda_II.markdown b/Yoneda_II.markdown
@@ -0,0 +1,237 @@
+# Yoneda Intuition from Humble Beginnings
+
+Let's explore the Yoneda lemma. You don't need to be an advanced Haskeller to understand this. In fact I claim you will understand the first section fine if you're comfortable with `map`/[`fmap`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor.html#v:fmap) and [`id`](https://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Function.html#v:id).
+
+I am not out to motivate it, but we will explore Yoneda at the level of terms and at the level of types.
+
+> "[Yoneda lemma], arguably the most important result in category theory."
+> 
+> [*What You Needa Know about Yoneda*](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/proyo.pdf)
+
+## Yoneda; Term level
+
+```haskell
+[1, 2, 3]
+```
+
+Every list can be expressed as a (higher-order) function by viewing it through our Yoneda-tinted glasses 🕶:
+
+```haskell
+\f -> [f 1, f 2, f 3]
+```
+
+It's like the function `f` grabs a hold of each element. I'll call it `post` because it does "postprocessing".
+
+The Yoneda lemma states that these are equivalent (naturally isomorphic)! 
+How do we go back? We pass it the identity function:
+
+```haskell
+  (\post -> [post 1, post 2, post 3]) id
+= [id 1, id 2, id 3]
+= [1, 2, 3]
+```
+
+We didn't need `(f)map`. The Yoneda form of `[1, 2, 3]` can be understood without it but it is `map` partially applied to its second argument:
+
+```haskell
+\post -> [post 1, post 2, post 3]
+=
+\post -> map post [1, 2, 3]
+=
+flip map [1, 2, 3]
+```
+
+This works for any `Functor`, the Yoneda forms of `Just True` and `Nothing` are
+
+```haskell
+\post -> Just (post True)
+\_    -> Nothing
+```
+
+And the Yoneda form of [`Const "abc"`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Functor-Const.html#t:Const) doesn't touch the string:
+
+```haskell
+\_ -> Const "abc"
+```
+
+Recall that functions are Functors too (`instance Functor ((->) a)` where `fmap = (.)`), which is where our head starts to hurt: The Yoneda form now transforms a **function** to a higher-order function, how does that work?
+
+Let's take the function `not` as an example, we pass the result of `not bool` to `post`:
+
+```haskell
+\post -> \bool -> post (not bool)
+```
+
+So we are really postcomposing `post` with `not`:
+
+```haskell
+\post -> post . not
+\post -> fmap post not
+```
+
+Or doing case analysis on the Boolean
+
+```haskell
+\post -> \case    -- -XLambdaCase
+  True  -> post False
+  False -> post True
+```
+
+## Yoneda; Type level
+
+Our first example used `Functor []`
+
+```haskell
+list :: [Int]
+list = [1, 2, 3]
+```
+
+So what is the type of the Yoneda form? (switching back from `post` to `f`)
+
+```haskell
+yoList :: (Int -> x) -> [x]
+yoList f = [f 1, f 2, f 3]
+```
+
+Interesting. Is this what you expected? 
+
+Before we had a list of `Int`s. Now we have a **polymorphic** higher-order function. The polymorphism is crucial for this to work, (warning: vague) think of it as grabbing every `Int` inside of `[Int]` and ripping them out, leaving a hole `x` behind (not to be confused with [typed holes](https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.html#typed-holes), this is a conceptual hole).
+
+I think about this like cocking a crossbow (no I don't know archercy, so this will be a funky mythological bow):
+
+The Yoneda form of `[Int]` is like a loaded crossbow: we have "pulled" the `Int` out of it `(Int -> x)`, leaving a list of holes `[x]`.
+
+To fire we take two steps:
+1. Remember that `yoList` actually takes `x` as an invisible argument: `forall x. (Int -> x) -> [x]`. This means our first step is to instantiate `x` with a type: with crucial use of the polymorphism of `yoList` we pick `Int` using [visible type applications](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#visible-type-application)
+
+    ```haskell
+    yoList @Int :: (Int -> Int) -> [Int]
+    ```
+2. The second step is passing `id :: Int -> Int` (..the arrow?) as an argument, and we get `yoList @Int id :: [Int]` back.
+
+Let's look at the other cases,
+
+```haskell
+just :: Maybe Bool
+just = Just True
+```
+becomes
+```haskell
+yoJust :: (Bool -> x) -> Maybe x
+yoJust f = Just (f True)
+``
+
+`Nothing :: Maybe a` contains no values of type `a` but, but we can still follow the pattern:
+```haskell
+yoNothing :: (a -> x) -> Maybe x
+yoNothing _ = Nothing
+```
+
+Similarly `constAbc` contains no values of `a` 
+```haskell
+constAbc :: Const String a
+constAbc = Const "abc"
+```
+so 
+```haskell
+yoConstAbc :: (a -> x) -> Const String x
+yoConstAbc _ = Const "abc"
+```
+
+You might ask, "what happens if we do want to change the `String`?". So far I have restricted myself to `Functor` which is very limiting. See if you can make sense of the type of `\f -> Const (f "abc")` or even
+```haskell
+yoPair :: (Int -> x) -> (x, x)
+yoPair f = (f 1, f 2)
+```
+
+which is not a Haskell `Functor`. We can in fact play this game with arbitrary type parameters;
+
+```haskell
+pair :: (Int, Bool, Char)
+pair = (10, False, 'X')
+
+yoPair1 :: (Int -> x) -> (x, Bool, Char)
+yoPair1 f = (f 10, False, 'X')
+
+yoPair2 :: (Bool -> y) -> (Int, y, Char)
+yoPair2 f = (10, f False, 'X')
+
+yoPair123 :: (Int -> x) -> (Bool -> y) -> (Char -> z) -> (x, y, z)
+yoPair123 f g h = (f 10, g False, h 'X')
+```
+
+etc. are you getting a feel for it yet? To go back, we pass `id`.
+
+Functions get weird though, when we have a function `show @Int` the type is
+
+```haskell
+show @Int :: (->) Int String
+```
+
+and `flip fmap show` (`(<$> show)`) pulls the `String` back
+
+```haskell
+(<$> show @Int) :: (String -> x) -> (Int -> x)
+```
+
+But the same doesn't work for `Int`, up until now we have worked on **co**variant arguments but `String` appears **contra**variantly. To understand the difference compare the type of `fmap` and [`contramap`](https://hackage.haskell.org/package/contravariant-1.5/docs/Data-Functor-Contravariant.html#v:contramap): the only difference is that the input arrow is flipped:
+
+```haskell
+fmap      :: Functor       f => (a -> a') -> (f a -> f a')
+contramap :: Contravariant f => (a <- a') -> (f a -> f a')
+```
+
+## Yoneda; Type level again
+This is starting to feel ranty, I will discuss how to actually use [`Yoneda`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html) later (for example to fuse `fmap`s or to derive right Kan extensions), but for now I leave you with the type of `fmap @F` (I'm jumping around with variable names):
+
+```haskell
+(a -> x) -> (F a -> F x)
+```
+
+What is the type of `flip (fmap @F)`?
+
+```haskell
+F a -> (a -> x) -> F x
+```
+or if you wish to be explicit
+```haskell
+forall a x. F a -> (a -> x) -> F x
+```
+
+It kind of looks like `F a` and `F x` are having a tug-o-war using `(a -> x)`. Of course that's not what is happening at all, perish the thought. But if we float the `forall x` past `F a`
+
+```haskell
+                 vvvvvvvvvvvvvvvvvvvvvvvvv
+forall a. F a -> forall x. (a -> x) -> F x
+                 ^^^^^^^^^^^^^^^^^^^^^^^^^
+```
+
+we got ourselves the type of our Yoneda forms. Because our `yo*` examples had to be polymorphic in the `x`
+
+```haskell
+yoList          :: forall   x. (Int    -> x) -> [x]
+yoJust          :: forall   x. (Bool   -> x) -> Maybe x
+yoNothing       :: forall a x. (a      -> x) -> Maybe x
+yoConstAbc      :: forall a x. (a      -> x) -> Const String x
+(<$> show @Int) :: forall   x. (String -> x) -> (Int -> x)
+```
+
+so with [`RankNTypes`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-RankNTypes) we can `Yoneda` a name (I use a type synonym for simplicity, you will want to use a `newtype` like [`Data.Functor.Yoneda`](https://hackage.haskell.org/package/kan-extensions-5.2/docs/Data-Functor-Yoneda.html#t:Yoneda))
+
+```
+>> :set -XRankNTypes
+>> type Yoneda f a = (forall xx. (a -> xx) -> f xx)
+>>
+>> :t (\f -> [f 1, f 2, f 3]) :: Yoneda [] Int
+.. :: (Int -> xx) -> [xx]
+```
+
+and now we 
+
+```haskell
+yoList          ::           Yoneda []             Int
+yoJust          ::           Yoneda Maybe          Bool
+yoNothing       :: forall a. Yoneda Maybe          a
+yoConstAbc      :: forall a. Yoneda (Const String) a
+(<$> show @Int) ::           Yoneda ((->) Int)     String
+```