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

A new Categories library for Agda

The agda-unimath library

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

Total Parser Combinators in 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.

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

A formalization of the polymorphic lambda calculus extended with iso-recursive types

Cartesian Cubical Type Theory

A cost-aware logical framework, embedded in Agda.

This aims to be the most pretentious implementation of stlc in existence

A work-in-progress core language for Agda, in Agda

Agda formalisation of second-order abstract syntax

A Logical Relation for Martin-Löf Type Theory in Agda

Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

Agda category theory library for denotational design

H.O.T.T. using rewriting in Agda

A formalized proof of a version of the initiality conjecture

antifunext

A formalization of M-types in Agda

A toy dependent typed language.

An attempt towards univalent classical mathematics in Cubical Agda.

Mechanizations of Type Theories

Intrinsic Verification of Formal Grammar Theory

An Agda formalization of System F and the Brown-Palsberg self-interpreter