# Function Types¶

Function types are written `(x : A) → B`

, or in the case of non-dependent functions simply `A → B`

. For instance, the type of the addition function for natural numbers is:

```
Nat → Nat → Nat
```

and the type of the addition function for vectors is:

```
(A : Set) → (n : Nat) → (u : Vec A n) → (v : Vec A n) → Vec A n
```

where `Set`

is the type of sets and `Vec A n`

is the type of vectors with `n`

elements of type `A`

. Arrows between consecutive hypotheses of the form `(x : A)`

may also be omitted, and `(x : A) (y : A)`

may be shortened to `(x y : A)`

:

```
(A : Set) (n : Nat)(u v : Vec A n) → Vec A n
```

Functions are constructed by lambda abstractions, which can be either typed or untyped. For instance, both expressions below have type `(A : Set) → A → A`

(the second expression checks against other types as well):

```
example₁ = \ (A : Set)(x : A) → x
example₂ = \ A x → x
```

You can also use the Unicode symbol `λ`

(type “\lambda” in the Emacs Agda mode) instead of `\\`

.

The application of a function `f : (x : A) → B`

to an argument `a : A`

is written `f a`

and the type of this is `B[x := a]`

.

## Notational conventions¶

Function types:

```
prop₁ : ((x : A) (y : B) → C) is-the-same-as ((x : A) → (y : B) → C)
prop₂ : ((x y : A) → C) is-the-same-as ((x : A)(y : A) → C)
prop₃ : (forall (x : A) → C) is-the-same-as ((x : A) → C)
prop₄ : (forall x → C) is-the-same-as ((x : _) → C)
prop₅ : (forall x y → C) is-the-same-as (forall x → forall y → C)
```

You can also use the Unicode symbol `∀`

(type “\all” in the Emacs Agda mode) instead of `forall`

.

Functional abstraction:

```
(\x y → e) is-the-same-as (\x → (\y → e))
```

Functional application:

```
(f a b) is-the-same-as ((f a) b)
```