Categories - Categories parametrized by morphism equality, in Agda. Agda Prelude - Alternative to the Agda standard library that focuses more on programming and type checking time performance. gen-cart - Unifying Cartesian Cubical Set Model. Generic - Library for doing generic programming in Agda. potpourri - Where everyday Agda research of G. Allais happens. AgdaBench - Benchmarking tool for compile-time performance of Agda programs. system-f-agda - Formalization of the polymorphic lambda calculus extended with iso-recursive types. calf - Cost-aware logical framework, embedded in Agda. agdarsec - Total Parser Combinators in Agda.