The Agda standard library

A new Categories library for Agda

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

An introductory course to Homotopy Type Theory

The agda-unimath library

Lecture notes on univalent foundations of mathematics with Agda

Compiling Agda code to readable Haskell

Agda formalisation of the Introduction to Homotopy Type Theory

The theory of algebraic graphs formalised in Agda

A cost-aware logical framework, embedded in Agda.

Agda category theory library for denotational design