Personal agda library. It is called willow because it needed a name.
This is the old version.
basic contains basic type theory stuff.
cat contains category theory.
cat2 is discontinued.
You need to call the repository directory on your computer 'willow' for the directory structure to work. This is so that you can easily refer to it as a library from parallel projects.
This is the new version.
basic contains basic type theory stuff.
cat contains category theory.
INTENDED IMPROVEMENTS OF willow2 OVER willow:
- Use of the standard library
- Use of instance arguments (but are they useful here?)
- For structure on types: yes
- For structure on functions: less so
- Use of irrelevance
- Level in the record (but currently using type-in-type)