Also check out Philip Wadler's Programming Language Foundations in Agda: https://plfa.github.io/