natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
Cubical Agda is a mode of Agda (turned on by the flag --cubical
) that implements a type theory similar to CCHM (De Morgan) cubical type theory, and thus a form of homotopy 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-Löf identity 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.
The guarded cubical variant extends cubical Agda to support guarded recursive definitions which can be used to formalize synthetic guarded domain theory.
Agda-flat
is a mode of Agda that 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:
Listed here are some little-known or undocumented features of Agda that are sometimes useful. Note that undocumented “features” may change without warning; this list is current as of September 2022, Agda v2.6.2.
There are a lot of useful documented keybindings that you may not be aware of.
C-c C-,
and C-c C-.
can be prefixed with C-u C-u
to normalize the type of the hole (and the term, in the second case) before displaying them.The manual doesn’t document the customizable variables in the Emacs mode. Of particular note are:
agda-input-user-translations
allows you to add new bindings to the Unicode input modeagda2-highlight-level
, when set to interactive
, uses highlighting to display realtime information about which terms and subterms in the buffer Agda is currently typechecking.agda2-program-args
allows you to add command-line arguments to be used every time (e.g. the -v
options below). This in in addition to the arguments specified by a particular file in the OPTIONS
line.To change the values of these variables, run M-x customize-variable RET
and enter the variable name, change the value, and then “Set and Save”.
The command -v
(verbose output) accepts various additional options that are, according to the developers, “documented by their implementation”. These include:
rewriting.rewrite:50
— displays information about attempted uses of rewrite rules.rewriting.match:60
— displays information about attempted matches during rewriting.import.chase:2
— when compiling imported files, displays a notification when each file is completed in addition to when it is started.Unfortunately, the output produced by these flags appears in the *Agda debug*
buffer, which is not visible by default, rather than the standard AgdaInfo
buffer. To turn these flags on, you can add (for instance) -v import.chase:2
to agda2-program-args
via Customization, as above, or to the OPTIONS
line of a particular file.
Since Agda has many experimental features under active development, bugs in these features are not uncommon. When reporting a bug, it is helpful to “minimize” it to make the shortest possible MRE. Some tips for doing this from the developers include
--type-in-type
, --no-termination-check
, --no-positivity-check
, --no-projection-like
, --no-fast-reduce
Agda.Builtin
modules)_
if they are not usedw/e
where w/e : ∀ {ℓ} {A : Set ℓ} → A
is a postulate_
in terms by their solutionbased on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Agda landing page:
Documentation:
Online Agda interface:
Plain Agda originates with:
Ulf Norell, Towards a practical programming language based on dependent type theory, PhD thesis (2007) [pdf, pdf]
Ulf Norell, Dependently Typed Programming in Agda, in: Advanced Functional Programming AFP 2008, Lecture Notes in Computer Science 5832 (2009) 230-266 [doi:10.1007/978-3-642-04652-0_5, pdf]
Textbook account:
Cubical Agda (an implementation of cubical type theory, for univalently computing homotopy type theory) originates with:
Anders Mörtberg, Cubical Agda (2018) [blog post]
Andrea Vezzosi, Anders Mörtberg, Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, Proceedings of the ACM on Programming Languages 3 ICFP 87 (2019) 1–29 [doi:10.1145/3341691, pdf]
Libraries for/with homotopy type theory/univalent foundations of mathematics:
original HoTT library: github.com/hott/hott-agda
(motivated towards univalent categories)
E.g. on group theory (cf. Symmetry):
Implementation of Cauchy real numbers (in Bishop-style constructive analysis) in Agda (cf. exact real computer arithmetic):
Martin Lundfall, Formalizing real numbers in Agda (2015) [pdf, pdf, github]
Zachary Murray, Constructive Analysis in the Agda Proof Assistant [arXiv:2205.08354, github]
Guillaume Brunerie, The Agda proof assistant (2012) [slides:pdf]
Ulf Norell, Programming in Agda, presentation at Oregon Programming Languages Summer School (2014) [lecture 1: video, 2: video, 3: video, 4: video]
Scott Fleischman, Agda from Nothing, talk at λC (2016) [video 1, video 2]
Philip Wadler, (Programming Languages) in Agda = Programming (Languages in Agda), talk at Codegram (Sep 2019) [video]
Fredrik Nordvall Forsberg, The basic syntax of Agda, talk at CS410 Advanced Functional Programming (2021) [video]
On cubical Agda:
General:
Dan Licata, Ian Voysey, Programming and proving in Agda, course material (2013)
Peter Selinger, Lectures on Agda (2021) [web]
Ingo Blechschmidt, Agda – a beautiful proof assistant, course at Teoria dei Tipi, Padova (Apr 2023) [webpage]
With emphasis on implementing homotopy type theory and univalent foundations of mathematics:
Guillaume Brunerie, Agda for homotopy type theory [github]
Martín Hötzel Escardó, Introduction to Univalent Foundations of Mathematics with Agda (2019) [arXiv:1911.00580, webpage]
Last revised on November 8, 2023 at 09:25:24. See the history of this page for a list of all contributions to it.