Agda is a dependently typed programming language / interactive theorem prover.

The Agda standard library

An experimental library for Cubical Agda

Development of homotopy type theory in Agda

An introductory course to Homotopy Type Theory

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

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

Lecture notes on univalent foundations of mathematics with Agda

A curated set of links to formal methods involving provable code.

agda-mode on VS Code

Categories parametrized by morphism equality, in Agda

agda-mode for neovim

Agda formalisation of the Introduction to Homotopy Type Theory

Total Parser Combinators in Agda

A SuperCompiler for Martin-Löf's Type Theory

Language Server for Agda

A slow-paced introduction to reflection in Agda. ---Tactics!

Agda bindings to SMT-LIB2 compatible solvers.

The theory of algebraic graphs formalised in Agda

A workshop on learning Agda with minimal prerequisites.