An introduction to programming language theory in Agda

The Agda standard library

An experimental library for Cubical Agda

Development of homotopy type theory in Agda

A new Categories library for Agda

An introductory course to Homotopy Type Theory

Programming library for Agda

The theory of algebraic graphs formalised in Agda

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality

Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages.

Cryptographic Constructions in the Type Theory of Agda

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

H.O.T.T. using rewriting in Agda

Proof automation – for Agda, in Agda.

A fast, easy-to-use ring solver for agda with step-by-step solutions

Agda programming with holes

A Dependently Typed Linear π-Calculus in Agda

Synthetic Differential Geometry in Agda

Semisimplicial types in Agda

This is an experimental base library which is supposed to contain functional datastructures and reflection code.