nLab Agda

Overview

A dependently typed functional programming language with applications to certified programming. It is also used as a proof assistant.

Besides Coq, Agda is one of the languages in which homotopy type theory has been implemented (Brunerie). Agda can be compiled to Haskell, Epic or Javascript.

Variants

Cubical Agda

Cubical Agda is a version of Agda (turned on by the flag --cubical) that implements a type theory similar to CCHM (De Morgan) cubical type theory.

Its main difference from CCHM is that instead of an exotype of “cofibrant propositions” it uses the interval itself, replacing cofibrant propositions by statements of the form $r \equiv 1$ for some dimension expression $r$. This change does not prevent the construction of a model for the theory in De Morgan cubical sets, although it doesn’t technically fall under the Orton-Pitts axioms since $I$ is not a subobject of $\Omega$, and no one has checked whether this model can be strengthened to a Quillen model category.

More problematically, to support identity types a la Swan (which are distinct from both cubical “path types” and Martin-Lof “identity types” – the latter sometimes called “jdentity types” to emphasize their definition relative to the J-eliminator) the type of cofibrant propositions must support a dominance. Cubical Agda thus assumes that $I$ supports a dominance, but this is not true in De Morgan cubical sets. So the semantics of the entirety of Cubical Agda, with Swan identity types, is unclear. (For this reason, the Cubical Agda library generally avoids using Swan identity types, although Cubical Agda supports them.)

Ordinary Martin-Lof jdentity types? should, in principle, also be definable in Cubical Agda as an indexed inductive family, with computational behavior as usual for any inductive types in cubical type theory. As of March 2021, however, there is a bug in Cubical Agda that prevents jdentity types from computing correctly.

Agda-flat

The variant Agda-flat implements a co-monadic modal operator $\flat$ (“flat”, following the notation used in cohesive homotopy type theory as introduced in dcct and type-theorertically developed in Shulman 15). This makes Agda model a modal type theory and hence a modal homotopy type theory, such as used, for instance, in Wellen 2017.

See:

• Agda-flat documentation

• installation instructions

Related concepts

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cubical Agda

  • library and demos

based on modal type theory:

• Agda-flat: installation instructions

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project

References

General information on Agda is at

• Agda Wiki

• ‘Hello World!’ in Adga

• learn-you-an-agda (and achieve enlightment)

• Ulf Norell, James Chapman, Dependently Typed Programming in Agda (pdf)

• Dan Licata, Ian Voysey, Programming and proving in Agda

• Ulf Norell, Towards a practical programming language based on dependent type theory, 2007 (pdf)

A tutorial for use of Agda as an implementation of homotopy type theory is at

• Guillaume Brunerie, Agda for homotopy type theory (web)

• Guillaume Brunerie, The Agda proof assistant, slides, pdf

and specifically of Cubical Agda as an implementation of cubical type theory:

• Andrea Vezzosi, Anders Mörtberg and Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, 2019 (pdf)

The HoTT-Agda library is at

• github, hott-agda

category: software