Agda is a dependently typed functional programming. Dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.
-
A dependent function's return type may depend on the value (not just type) of an argument. A function that takes a positive integer "n" may return an array of length "n".
-
A dependent pair may have a second value that depends on the first. It can be used to encode a pair of integers where the second one is greater than the first.
A definition is a syntactic construction defining an entity such as a function or a datatype.
f : (x : A) → B
is a dependently typed function, i.e. x can occur in B.
When B does not depend on x we write f : A → B