# Core Syntax

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[n] variable | abstraction | application | function space | universe

(The optional `n`

following `Set`

denotes a level; the default is 0.)

Terms must be well-scoped and well-typed. To be more precise, see the typing rules.