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 : Type) → (n : Nat) → (u : Vec A n) → (v : Vec A n) → Vec A n

where Type is the type of small types 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) (see also telescopes):

(A : Type) (n : Nat)(u v : Vec A n) → Vec A n

Functions are constructed by lambda expressions or Function Definitions.

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)