An introduction to programming language theory in Agda

Development of homotopy type theory in Agda

An introductory course to Homotopy Type Theory

Learn you an Agda (and achieve enlightenment)

Logical manifestations of topological concepts, and other things, via the univalent point of view.

being the lecture materials and exercises for the 2017/18 session of CS410 Advanced Functional Programming at the University of Strathclyde

Lecture notes on univalent foundations of mathematics with Agda

A workshop on learning Agda with minimal prerequisites.

Learn the Agda basics in three 2-hour sessions.

Like "Write Yourself a Scheme in 48 Hours", but in Agda

Basics of the dependently-typed functional language Agda ^_^