Verified Functional Programming in Agda Chapter 1 - Functional Programming with the Booleans Chapter 2 - Theorem Proving with the Booleans Chapter 3 - Natural Numbers Chapter 4 - Lists Chapter 5 - Internal Verification