Learning Agda one Proof at a time

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:

Read the docs

– Simon Beaumont 2022

There seems to be some duplication of stuff in here

See: Relations and Inequality for example.

Be good if the whole thing compiled into a library.

Translate all this into Lean4?