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.
agda-language-server - Language Server Protocol for Agda.
Gradual Typing in Agda - Formalizations of Gradually Typed Languages in Agda.
agda-algebras - The Agda Universal Algebra Library.
system-f-agda - Formalization of the polymorphic lambda calculus extended with iso-recursive types.
calf - Cost-aware logical framework, embedded in Agda.