A type theory satisfies canonicity if every term computes to a canonical form, built explicitly using the constructors of its type.

Handy links: