The Agda standard library

A new Categories library for Agda

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

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

Categories parametrized by morphism equality, in Agda

Total Parser Combinators in Agda

Agda formalisation of the Introduction to Homotopy Type Theory

The theory of algebraic graphs formalised in Agda

Algebra of Programming in Agda: Dependent Types for Relational Program Derivation

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

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

Cartesian Cubical Type Theory

Inline, type safe X86-64 assembly programming in Agda

A cost-aware logical framework, embedded in Agda.

Miller/pattern unification in Agda

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

A formalization of category theory in cubical Agda

Minimalistic dependent type theory with syntactic metaprogramming

Observational Type Theory as an Agda library

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

Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages.

Like "Write Yourself a Scheme in 48 Hours", but in Agda

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

Paradoxes of type theory, described didactically. With accompanying proofs in Agda.

A fast, easy-to-use ring solver for agda with step-by-step solutions

Base library for HoTT in Agda

Work in progress

antifunext

IO using sized types and copatterns