This is my work through the Programming Language Foundations in Agda book by Wen Kokke and Philip Wadler.