Canonicity of a Type Theory

A type theory satisfies canonicity if every closed term is definitionally equal to a "canonical value" of the same type. In intuitive terms, this means that we can evaluate closed terms, though we may not necessarily be able to normalize open ones.