-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2018.Yoneda
by Jannis Limperg
The talk will contain a full proof, which will require us to revisit and exercise much of the material from our previous Category Theory lectures. (Actually, that's perhaps the main benefit of the talk. The proof itself is complicated but kind of boring.) Time permitting, I'll also talk a bit about applications of the lemma.
The talk will closely follow my blog post on the topic [1], in case you want to get a sneak peak.
I've prepared a branch of my Category Theory formalisation with lots of holes in the proof of Yoneda's Lemma. You can try to fill in these holes as an exercise for the talk. However, be aware that there's quite a bit of notational overhead compared to the informal proof, so I'm not sure how enlightening this exercise will be.
The branch is at
tmp-exercise,
file Cats/Functor/Yoneda.agda. For solutions, see the same file in
the master branch.
- Jannis Limperg. Yoneda's Lemma in Excruciating Detail. 2018. Personal blog post.