FunctionSyntax

Function types are written (x : A) -> B or A -> B for non-dependent functions. Function types can range over arbitrary telescopes, for instance, the type of the substitutivity law for a polymorphic equality

 Eq : (A : Set) -> A -> A -> Set

can be stated as

 (A : Set)(C : A -> Set)(x y : A) -> Eq A x y -> C x -> C y

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):

 \ (A : Set)(x : A) -> x
 \ A x -> x