# Type synonyms

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

``\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``````