Mathematical proofs in Agda
This is an ongoing project for me to formalise my lecture notes from the Cambridge Mathematical Tripos. I started in about June 2018 and have been going at least through January 2019. I'm starting at the very beginning (a very good place to start), and proving as much as I can from the lecture notes and the example sheets.
I make no promises about the quality of this code. It's proofs, not prose.
Similarly, I'm using this to try and discover the right ways to do programming in a dependently-typed language, finding idioms and features as I go. Some of this was done really early, and the code is accordingly bad.
Some of the code might not compile; I'll try and make sure that it does compile as I commit to it, but I just wanted to get it up here first.
The code used to be versioned with Pijul.