An introduction to programming language theory in Agda

The Agda standard library

An experimental library for Cubical Agda

A new Categories library for Agda

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

The agda-unimath library

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

Compiling Agda code to readable Haskell

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

Merge sort correctness proof

A series of exercises for learning Category Theory in Agda