References#

• Programming Language Foundations in Agda – by Philip Wadler, Wen Kokke and Jeremy Siek
• Programming and Proving in Agda – by Jesper Cockx
• Introduction to Univalent Foundations of Mathematics with Agda – by Martín Escardó
• Dependent Types at Work – by Ana Bove and Peter Dybjer
• Learn you an Agda – by Liam O’Connor-Davis with additions by William DeMeo
• A practical Agda tutorial – by Péter Diviánszky and Ambrus Kaposi
• Correct-by-construction programming in Agda – by Jesper Cockx
• More on the double-negation translation
• Interactive Theorem Proving – by Thorsten Wißmann
• 1Lab – by Amélia Liao and collaborators
• TypeTopology – by Martín Escardó and collaborators