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

• UpdatedMar 15, 2025
• Haskell

The Agda standard library

• UpdatedMar 17, 2025
• Agda

An experimental library for Cubical Agda

• UpdatedMar 4, 2025
• Agda

Development of homotopy type theory in Agda

• UpdatedFeb 19, 2019
• Agda

An introductory course to Homotopy Type Theory

• UpdatedJul 24, 2020
• Agda

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

• UpdatedMar 17, 2025
• Agda

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

• UpdatedMar 13, 2025
• Agda

Lecture notes on univalent foundations of mathematics with Agda

• UpdatedApr 16, 2024
• Agda

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

• UpdatedDec 12, 2021

agda-mode on VS Code

• UpdatedMar 11, 2025
• ReScript

Categories parametrized by morphism equality, in Agda

• UpdatedAug 9, 2019
• Agda

agda-mode for neovim

• UpdatedFeb 20, 2025
• Haskell

Total Parser Combinators in Agda

• UpdatedMay 12, 2023
• Agda

Agda formalisation of the Introduction to Homotopy Type Theory

• UpdatedNov 27, 2021
• Agda

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

• UpdatedJan 29, 2022
• Scala

Language Server for Agda

• UpdatedDec 18, 2024
• Haskell

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

• UpdatedMay 25, 2022
• Agda

Agda bindings to SMT-LIB2 compatible solvers.

• UpdatedOct 7, 2024
• Agda

The theory of algebraic graphs formalised in Agda

• UpdatedJul 15, 2018
• Agda

A toolkit for enforcing logical specifications on neural networks

• UpdatedMar 17, 2025
• Haskell