Type classes
- Haskell vs. Agda type classes (simple vs. dependent types)
- Agda instance search
- a simple type class plus instances
- a medium type class
- a complicated type class plus instances

Prelude examples
- tabsToSpaces
- Calculator

? Finger trees
(Haskell's GADT)