nLab Agda

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Constructivism, Realizability, Computability

Contents

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 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 r1r \equiv 1 for some dimension expression rr. 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 II 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 II 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.

Guarded Cubical Agda

The guarded cubical variant extends cubical Agda to support guarded recursive? definitions which can be used to formalize synthetic guarded domain theory.

Agda-flat

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:

Little-known features

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.

    • This appears not to be documented in the manual (although it is in the Emacs docstring): When in a hole, the commands 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 mode
    • agda2-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.

Minimizing bugs

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

  • Enable --type-in-type, --no-termination-check, --no-positivity-check, --no-projection-like, --no-fast-reduce
  • Disable unused flags
  • Remove unused imports
  • Copy definitions from imported modules (other than Agda.Builtin modules)
  • Delete unused definitions
  • Turn functions into postulates
  • Inline functions
  • Remove clauses from definitions
  • Replace patterns by _ if they are not used
  • Replace types by Set
  • Delete unused arguments to functions or constructors
  • Remove dependencies from types
  • Replace (sub)terms by w/e where w/e : ∀ {ℓ} {A : Set ℓ} → A is a postulate
  • Make implicit arguments explicit
  • Replace wildcards _ in terms by their solution

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

based on cubical type theory:

based on modal type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

References

General information on Agda is at

With emphasis on the dependent type theory-aspect:

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

  • Ulf Norell, Dependently Typed Programming in Agda, p. 230-266 in: Advanced Functional Programming AFP 2008. Lecture Notes in Computer Science 5832 (2009) [doi:10.1007/978-3-642-04652-0_5, pdf]

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

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

On homotopy type theory and univalent foundations of mathematics in/with Agda:

The HoTT-Agda library is at

category: software

Last revised on October 8, 2022 at 02:27:36. See the history of this page for a list of all contributions to it.