________________________________________________________________________
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
Also a nice read is Certainty by Construction which is an altogether more gentle introduction to Agda by Sandy McGuire aimed at the general reader rather than a CS major; but as ever Sandy has been in quite deep and disovered a few Agda hints, tip and techniques which are not documented elsewhere (other then the reference manual I guess).
________________________________________________________________________
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 the awesome hen herself.
– Simon Beaumont 2022-2024
See: Relations and Inequality for example. That might be due to me jumping
around a bit.
I think more or less we eat our own dogfood where we can in each chapter. I know the standard-library is more robust and I take a peek if I think there’s anything subtle required in making sure we build our house on sound foundations it’s a great source of learning too.
Might make a chapter on this soon. As I followed a couple of Anders Mortberg
lectures on the HoTT Spring school and was captured when we did funext
and univalence in a couple of lines.