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

Page last modified on August 18, 2007, at 09:50 am

Powered by
PmWiki