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

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

Programming library for Agda

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT

Agda formalisation of the Introduction to Homotopy Type Theory

Agda bindings to SMT-LIB2 compatible solvers.

The Evolution of a Typechecker

A Brainfuck interpreter written in Agda

A TACtic library for Agda

A formalized proof of a version of the initiality conjecture

Proof automation – for Agda, in Agda.

Algebraic proof discovery in Agda

A toy dependent typed language.

A Unifying Cartesian Cubical Set Model

antifunext

Implementing grep in Agda

An attempt towards univalent classical mathematics in Cubical Agda.

Normalization by evaluation of simply typed combinators.

quotient types in cubical Agda

Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.

A formalization of the theory behind the mugen library

Meta-theory and normalization for Fitch-style modal lambda calculi

Simply-typed lambda calculus as a QIT in cubical Agda + normalization

Agda formalisation of FOTC (First-Order Theory of Combinators).