Yoneda
# Category Theory
In this post, I assume the bunch of terms in the language "category theory", or the "presheaf theory".
## The notation of presheaves
Let $\mathscr{C}$ be a category. I use the following conventions for presheaf theory.
- $\mathscr{\hat C} := [\mathscr{C}^{op}, Set] := Hom_{Cat}(\mathscr{C}^{op}, Set)$
- $\mathscr{\check C} := [\ \mathscr{C}\ \ , Set] := Hom_{Cat}(\ \mathscr{C}\ \ , Set)$
We call the first functor category the category of presheaves over $\mathscr C$, while the second one the category of copresheaves over $\mathscr C$.
In addition to this, I use the notation $\mathscr{\check y}$ for the (op)yoneda embedding $(x \mapsto Hom_\mathscr{C}(x,-))$ and $\mathscr{\hat y}$ for the yoneda embedding $(x \mapsto Hom_\mathscr{C}(-,x))$.
A Beginner might be careful about the sensitivity between $Hom$ functors;
- $\mathscr{\check y_\mathscr C}(A) := Hom_\mathscr{C}(A,-)$ is a covariant functor
- $\mathscr{\hat y_\mathscr C}(A) := Hom_\mathscr{C}(-,A)$ is a contravariant functor
and yoneda embeddings;
- $\mathscr{\check y_\mathscr C}$ is a contravariant functor
- $\mathscr{\hat y_\mathscr C}$ is a covatiant functor
When we do not need to specify $\mathscr C$ explicitly, I often use the notation $\mathscr{\hat y}$ and $\mathscr{\check y}$ for $\mathscr{\hat y_\mathscr C}$ and $\mathscr{\check y_\mathscr C}$ respectively. Also, I use $Hom(*,-)$ for $Hom_\mathscr C(*,-)$ . Although I do not introduce explicitly "internal hom" which is defined as a exponential in a proper setting, I will show how morphisms are `internalized` and objects are `externalized` in this post.
## A caution about $Hask$
$Hask$ is not a category precisely.
However, I would like $Hask$ to be a category here.
It might be harmful to exclude from Hask all the fact that could be applied to complete version of $Hask$ .
# Yoneda Lemma
OpYoneda Lemma
$$Hom_\mathscr{\check C}(\mathscr{\check y}(A),F) = F(A)$$
Yoneda Lemma
$$Hom_\mathscr{ \hat C}(\mathscr{\hat y}(A),F) = F(A)$$
I use the convention that Yoneda Lemma refers, strictly speaking, to the Lemma that the functor $F$ is contravariant, since it inhabits the field of "presheaf" theory and not "copresheaf", i.e. the field of "homology" rather than "cohomology". The covariant Yoneda Lemma would be called "coYoneda" Lemma. However an ambiguity occurs here. The "coYoneda" Lemma is reserved for another Yoneda Lemma which is introduced with ∞-category and Grothendieck constructions later in the chapters. There is Homotopy Theory behind this kind of usage of Co-natation which might seem a bit different from category theory. You might know cocylinder, comaps, cofibrations, copath, and so on. These are terms used in Homotopy Theory. ∞-category is backboned by homotopy theory and hence we would like to reserve "coyoneda" for ∞-category theory. So, here we call the covariant-version of Yoneda Lemma as "OpYoneda" Lemma.
However, since OpYoneda Lemma is the trivial reverse of Yoneda Lemma, I may call the both "Yoneda" and "OpYoneda" Lemma as Yoneda Lemma later on this post.
## Yoneda Lemma in Haskell
Yoneda Lemma is composed by a bijection
$$\phi : Hom_\mathscr{\check C}(\mathscr{\check y}(A),F) \to F(A)$$
such that $\phi(\theta)$ is an element of $F(A)$ where $\theta$ is a natural transformation.
Hence its type $Hom_\mathscr{\check C}(\mathscr{\check y}(A),F)$ can be rewritten with;
$$\forall K. Hom_\mathscr{\check C}(Hom_\mathscr{C}(A,K),F(K))$$
This is
~~~ haskell
∀ K . (A → K) → F K
~~~
So in Haskell, Yoneda Lemma is written to be that a morphism $\phi$;
~~~ haskell
phi :: (∀ K . (A → K) → F K)) → F A
~~~
is a bijection. That is, there is an inverse morphism $\psi$;
~~~ haskell
psi :: F A → (∀ K . (A → K) → F K))
~~~
such that;
~~~ haskell
psi . phi == id
phi . psi == id
~~~
## Implementation of Yoneda Lemma
Given a category $\mathscr C$ and a contravariant functor $F : \mathscr C^{op} \to Set$, `externalize` is a technique of using the category of presheaves $\mathscr{\check C}$ to see the object $F(C)$ in the category $Set$. In other words, the inside of a set $F(C)$ can be seen as a external morphism in the functor category $\mathscr{\check C}$ i.e. natural transformation. The `internalize` is the inverse of `externalize`. With `internalize`, an externally existing morphism out of objects in the category of presheaves can be seen as an inhabitant of a particular set.
In a trivial case, `externalize` is yoneda embedding itself. Or, as an object, functor $F$ is precisely composed of some or many yoneda embedded objects from category $\mathscr C$. ( For more details, see the defintion of ∞-category on the category of simplicial sets. It's the best way to feed the intuition. )
Thus, in terms of presheaf theory, Yoneda Lemma shows that `internilize` and `externalize` compose an equivalence. Then let's see the `op` version of the above argument, i.e. functors are covariant living in the category of copresheves $\mathscr{\check C}$.
~~~ haskell
{--
#################################
## Yoneda Lemma ##
#################################
--}
{-# LANGUAGE UnicodeSyntax #-}
module Yoneda where
internalize :: Functor f => (∀ k. (a→k)→f k) → f a
internalize t = t id
externalize :: Functor f => f a → (∀ k. (a→k)→f k)
externalize a k = fmap k a
-- such that;
-- internalize . externalize ~~ id
-- externalize . internalize ~~ id
~~~
where functional extentionality gives `~~` equality `==`.
## The proof in Haskell like Notation
The proof is given by
~~~ haskell
int = internalize
ext = externalize
{--
int (ext a)
= (ext a) id [defn of int]
= fmap id a [defn of ext]
= id a [property of fmap]
= a [defn of id]
ext (int t) k
= ext (t id) k [use defn of int]
= fmap k (t id) [use defn of ext]
= (fmap k) (t id) [left assoc]
= (fmap k) ((ext t*) id) [exists t* , ext t* == t]
= (ext t*) (fmap k id) [k natural]
= (ext t*) (k . id) [defn of fmap for ((>>) a)]
= k t [now, defn of t*]
--}
~~~
I assumed the naturality of a functor `k` i.e. `(ext k) . (fmap g) = (fmap g) . (ext k)` ,
although, this is true as the following proof;
~~~ haskell
{--
ext k (fmap g x)
= fmap (fmap g x) k [defn of ext]
= fmap (g . x) k [defn of fmap for ((->) a)]
= (fmap g . fmap x) k [property of fmap]
= fmap g (fmap x k) [defn of (.)]
= fmap g (ext k x) [defn of ext]
= (fmap g . ext k) x [defn of (.)]
--}
~~~
# Examples of (Op)Yoneda Lemma
OpYoneda Lemma assumes an existence of a covariant functor $F$.
Here I provide three examples of the functor $F$;
1. $F = Id$
2. $F = List$
3. $F = Hom(C,-)$
Let's see the definition of these functors in Haskell.
1. Functor $Id$ or `I` is defined as follows;
~~~ haskell
data I a = I a
instance Functor I where
fmap f (I a) = I (f a)
~~~
2. Functor $List$ or `[ ]` is defined in GHC, e.g;
~~~ haskell
data [a] = [] | (:) a [a]
instance Functor [] where
fmap f [] = []
fmap f (x:xs) = f x : fmap f xs
~~~
3. Functor $Hom(C,-)$ or `((->) c)` is defined as follows;
~~~ haskell
instance Functor ((->) c) where
fmap f = (.) f
~~~
## Continuation Passing Style
`CPS a` is a type of natural transformations in OpYoneda Lemma where $F = Id$
~~~
type CPS a = ∀ k . (a → k) → k.
~~~
CPS(a) is the externalization of `Id(a)` such that;
~~~ haskell
toCPS :: a → (∀ k . (a → k) → k)
toCPS a f = f a
~~~
while the internalization is given by
~~~ haskell
fromCPS :: (∀ k . (a → k) → k) → a
fromCPS t = t id
~~~
As we see later, `toCPS` is a variant of yoneda embedding $\mathscr{\check y}$ itself.
Thus, we have beautiful typings of CPS as the followings;
- `toCPS` : $\mathscr{C} \rightarrow \mathscr{\check C}$
- `fromCPS` : $\mathscr{\check C} \rightarrow \mathscr{C}$
where $\mathscr C$ is a kind of $Hask$ .
## Reverse Engineering Machines (CPSs)
![](/image/machine2.jpg width="600")
A picture from [A Neighborhood of Infinity](http://blog.sigfpe.com/2006/11/yoneda-lemma.html?m=1)
When $F = List$, the Yoneda Lemma gives us the listed version of CPS transformation.
`toCPSs` is a function which, given a list of terms, returns list of CPS terms.
~~~ haskell
toCPSs :: [a] → (∀ b . (a → b) → [b])
toCPSs ass f = map f ass
fromCPSs :: (∀ b . (a → b) → [b]) → [a]
fromCPSs t = t id
~~~
A set of CPS terms is like this;
~~~ haskell
CPS_tms :: ∀ b . (a → b) → [b]
CPS_tms f = map f tms
where tms = undefined
~~~
CPS transformated terms might be good when it is reversed;
~~~ haskell
CPS_tms' :: ∀ b . (a → b) → [b]
CPS_tms' f = reverse $ map f tms
where tms = (undefined)
~~~
Instead of reverse we could use any function `[a] → [a]` and we'd still get a sensible result out of `toCPSs`.
~~~ haskell
CPS_tms'' :: ∀ b . (a → b) → [b]
CPS_tms'' f = map f tms
where tms = reverse $ (undefined)
~~~
The reason is that if `f` is of type `∀ a.[a] → [a]` then `f $ map g a` equals `map g $ f a`. So we can rewrite `CPS_tms'` as
## Yoneda Embedding itself $\mathscr {\check y}$
Yoneda embedding $\mathscr {\check y}$ is represented in the situation of
$F = Hom(C,-)$ .
Yoneda Embedding $\mathscr {\check y}$ is a contravatiant functor and hence,
it is the primitive model of CPS transformation or the Categorical Version of CPS transformation which flips the order of function applications.
( See the following section. )
~~~ haskell
int :: (∀ k . (a→k) → (c→k)) → (c→a)
int t = t id
opyoneda :: (c→a) → (∀ k . (a→k) → (c→k))
opyoneda g k = k . g
~~~
`opyoneda` is OpYoneda Embedding $g ↦ (-∘g)$ i.e. ;
$$ \mathscr{\check y} : Hom_\mathscr{C}(C,A) ⭇ Hom_\mathscr{\check C}(Hom_\mathscr{C}(A,-),Hom_\mathscr{C}(C,-))$$
or
$$ \mathscr{\check y} : Hom_\mathscr{C}(C,A) ⭇ Hom_\mathscr{\check C}(\mathscr{\check y}(A),\mathscr{\check y}(C))$$
~~~ haskell
opyoneda_g :: ∀ k . (a→k) → (c→k)
opyoneda_g f = f . g
where g x = undefined
~~~
## CPS in Category Theory Style
The codes in this section are pseudo-codes. So we cannot run the codes in Haskell interpreters without some modifications.
The CPS Transformation on Type `K` is a Copresheaf Functor over the category `Hask`.
~~~ haskell
CPS(K) :: Hask → Hom(Hask,Set)
CPS(K) := Hom(Hom(-,K),K)
CPS(K) f = - . f
~~~
CPS transformation is just a Yoneda.
Its preudo-Haskell-like syntax is written as follows;
~~~ haskell
CPS :: Hask → (B→A) → (A→K) → (B→K)
CPS [K] f k = k . f
~~~
Taking quantification on `K`, and substituting `B = 1`, we will get;
~~~ haskell
type CPS A = ∀K . (A→K)→K
~~~
Now we define the Syntax of categorical version of STL (Simply Typed Lambda) Calculus as follows;
~~~ haskell
t ::= x
| λx.M
| (M . N)
~~~
Assuming a new Notation `(-)* := CPS`, we get;
~~~ haskell
(x)* k := k . x
(λx.M)* k := k . (λx.M)
= M* . (λm.k(λx.m))
(M . N)* k := k . (M . N)
= M* . (λm.k . (m . N))
= M* . (λm.N* . (λn.k(m . n)))
~~~
Here, nonCPS term `t` is got by `t == t* id id` .
The first argument `id` is the continuation of `t` which is the most outer continuation (or the last continuation).
The second argumennt `id` is the element of Unit Type `1` with which one can get elements in Category Theory.
# ∞-Category Theory
From here, we assume the basics of ∞-category theory. Particularly, we use the theory of presheaves and Grothendieck Constructions. For more detail see [Cisinski](http://www.mathematik.uni-regensburg.de/cisinski/CatLR.pdf).
# CoYoneda Lemma
Let $F:C\to Set$ be a covariant $C$-module ("copresheaf").
The OpYoneda Lemma was right extension along the identity:
$$\int_k [C(-,k),F(k)] \simeq F$$
That is
~~~ haskell
(∀ K . (A → K) → F K)) ≃ F A
~~~
is a bijection.
The CoYoneda Lemma is left extension along the identity:
$$F \simeq \int^k F(k)\times C(k,-)$$
That is
~~~ haskell
F A ≃ (∃ K . F K × (A → K))
~~~
is a bijection.
# Examples of Coyoneda Lemma
## Closure
Think of the type of the following term;
~~~ haskell
let x = 3 in λy → x + y
~~~
which is clearly, say, the form of `a → b` type.
Using $Closure$ technique, the above term is converted into;
~~~ haskell
let x = 3 in ([x:3], λΓ → λy → let x = Γ.x in x + y )
~~~
whose type is `∃ Γ . Γ × (Γ → a → b)`
So let's prove;
~~~ haskell
a → b ≃ ∃ Γ . Γ × (Γ → a → b)
~~~
making use of CoYoneda Lemma.
## Proof
Coyoneda Lemma is
~~~ haskell
F A ≃ (∃ Γ . (A → Γ) × F Γ)
~~~
Now, substituting `F := - → a → b` and `A := 1` to the Lemma, we get;
~~~ haskell
1 → a → b ≃ ∃ Γ . (1 → Γ) × (Γ → a → b)
~~~
which is equivalent to
~~~ haskell
a → b ≃ ∃ Γ . Γ × (Γ → a → b)
~~~
Q.E.D.
# Appendix
## funny stuff
From [A Neighborhood of Infinity](http://blog.sigfpe.com/2006/11/yoneda-lemma.html?m=1)
Consider the following compiled using GHC with `-fallow-overlapping-instances -fglasgow-exts`:
~~~ haskell
class Test a where
f :: a -> a
instance Test a where
f = id
instance Test Int where
f x = x+1
~~~
`f` is the identity for everything except for objects of type Int.
This is an example of what they call "funny stuff".
## caron $\check C$
From [A Neighborhood of Infinity](http://blog.sigfpe.com/2006/11/yoneda-lemma.html?m=1)
The accent on this letter 'č' is called a caron or háček.
The book from which I learned about the Yoneda lemma used the caron to indicate the function I call check.
I called it that because the TeX command to produce this symbol is `\check`.
This is a multilayered pun, presumably by Knuth.
It could just be that 'check' is an anglicised abbreviation for háček.
But it's also a characterisically Czech accent so it's probably also an easier (for English speakers) spelling for 'Czech'. And I think it's also a pun on Čech.
The caron is used on an H to represent Čech cohomology and so it's also called the 'Čech' accent. (I hope you can read those characters on a PC, I wrote this on a Mac.)
## References
* [A Neighborhood of Infinity](http://blog.sigfpe.com/2006/11/yoneda-lemma.html?m=1)
* [ghasshee: CPS](/functional/2021-04-01-CPS.md/)
* [Closure in Coyoneda](http://prl.ccs.neu.edu/blog/2017/08/28/closure-conversion-as-coyoneda/)
* [Kashiwara Schapira: Categories and Sheaves](https://link.springer.com/book/10.1007/3-540-27950-4)
* [Cisinski: Higher Categories and Homotopical Algebra](http://www.mathematik.uni-regensburg.de/cisinski/CatLR.pdf)