DependentlyTyped

See the official user manual for the most up-to-date version of the information on this page.

At its core, Agda is a dependently typed lambda calculus. The grammar of terms is as follows.

 a ::= x         | λ x → a     | a a         | (x : a) → a    | Set
       variable  | abstraction | application | function space | universe