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 formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Lecture notes on univalent foundations of mathematics with Agda

Compiling Agda code to readable Haskell

Agda formalisation of the Introduction to Homotopy Type Theory

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

Cryptographic Constructions in the Type Theory of Agda

A TACtic library for Agda

Agda experiment to define Probability, Preference, Gambles, Superpositions, Utility, and "Qtility"

reading group

hashlattice in Rust