Category Theory in Agda - Learning exercise.
Categories - Categories parametrized by morphism equality, in Agda.
Introduction to Agda (2011) - Daniel Peebles' Introduction to Agda, presented at Boston Haskell.
Agda Prelude - Alternative to the Agda standard library that focuses more on programming and type checking time performance.
Agda from Nothing - Workshop on learning Agda with minimal prerequisites.
gen-cart - Unifying Cartesian Cubical Set Model.
Generic - Library for doing generic programming in Agda.
hilbert-gentzen - Agda formalisation of IPC, IS4, ICML, and ILP.
potpourri - Where everyday Agda research of G. Allais happens.
categories-agda library - Standard Category Theory library for Agda.
AgdaBench - Benchmarking tool for compile-time performance of Agda programs.