Type Substitution

type-theory

Definition

Type Substitution

A type substitution is a finite partial map from type variables to types.

Formally, for a set $\mathcal{A}$ of type variables and a universe $\mathcal{T}$ of types,

$$S:\mathcal{A}\rightharpoonup \mathcal{T}.$$

Applying $S$ to a type $\tau$ means replacing every type variable $\alpha \in \mathrm{dom}(S)$ occurring in $\tau$ by $S(\alpha )$.