Following these great courses: ________________________________________________________________________________
Mainly the first part of:
Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022.
With much practical help from:
Jesper Cockx - Programming and Proving in Agda. https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf
And some ideas and inspiration (as well as convincing me (by contradiction) that unicode ligagtures and symbols are good for readability if used with sparsity and taste :)
Conor McBride - CS410 Advanced Functional Programming University of Strathclyde lecture series 2017 https://github.com/pigworker/CS410-17.git Video set compiled by Philip Zucker: https://www.youtube.com/playlist?list=PLqggUNm8QSqmeTg5n37oxBif-PInUfTJ2
________________________________________________________________________________
With thanks to the instructors and their students for the all the Agda foo and sharing the joy of machine checked proof.
And of course massive kudos and gratitude to the creators and maintainers of Agda itself:
– Simon Beaumont 2022
See: Relations and Inequality for example.