An introduction to programming language theory in Agda

Development of homotopy type theory in Agda

A new Categories library for Agda

An introductory course to Homotopy Type Theory

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

Categories parametrized by morphism equality, in Agda

Agda formalisation of the Introduction to Homotopy Type Theory

being the materials for CS410 Advanced Functional Programming in the 2014-15 session

Summer school on programming in Agda

Showing how some simple mathematical theories naturally give rise to some common data-structures

being a collection of Agda-facilitated ramblings

Solutions of the exercises of the HoTT book

A Dependently Typed Linear π-Calculus in Agda

A personal library, formalizing cohesive homotopy type theory in Agda.

Programming Language Foundations in Agda