Dependently Typed

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