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

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

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

ECMAScript back end for Functional Reactive Programming in Agda

being bits and pieces I'm inclined to leave lying around

An implementation of Functional Reactive Programming

Agda programming with holes

Machine-checked Agda formalization for the ILC project

Agda proofs of the HoTT book exercises