Agda has three basic types: functions, products (records), and sums (data types). The first two of these use dependent types, i.e., a type may depend on a value. Using dependent types makes it natural to blur the distinction between types and values. Both of these now share the same expression language and the number of language concepts can be kept at a minimum.
Variables
Meta variables (goals)
Applications
Functions
Function type
Data types
Constructors
Case expressions
Records
Record selection
Record types
Let expressions
Open expressions