This repository collects examples of things I have learned while studying Agda. Posts in here are written in Literate Agda using Markdown so that they can be rendered nicely in GitHub.

However, these files can also be loaded by Agda and I encourage the reader to do this.

Modules in here should be self-contained and get posted here usually after I experienced some kind of difficulty learning something. If I spent more than an hour trying to define something "easy" it'll probably end up here.