Type synonyms

A type synonym is a function that returns a type and does not evaluate. To define a type synonym, use \type keyword:

\type T p_1 ... p_n => E

For example, we can define the type of pairs as follows

\type Pair (A : \Type) => \Sigma A A

This differs from the analogous function definition because Pair A and \Sigma A A are not computationally equivalent. Nevertheless, these types are equivalent. The coercion between them is implicit:

\func coerceFrom (p : Pair Nat) : \Sigma Nat Nat => p
\func coerceTo (p : \Sigma Nat Nat) : Pair Nat => p