# What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?

If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $$0:\mathbb{N}$$ is constructed when defining $$\mathbb{N}$$ and does not reduce to anything else.

But if we are in a pure Martin-Löf type theory then any inhabitant of any type ultimately refers to $$*:\mathbf{1}$$. Is there a name for this property (akin to normalization/canonicity)?

• Firstly, you should be a bit more specific about what "pure Martin-Löf type theory" is supposed to be, as most people would include $\mathbb{N}$ in that. Secondly, the identity function $\lambda x : \mathbf{1} \,.\, x$ is a closed term of type $\mathbf{1} \to \mathbf{1}$ which does not refer to $\star$. The premises of your question is either false or inaccurate. Jan 23, 2021 at 8:05
• I think the author is asking if there is a name for a type theory in which every term is contractible. These type theories are entirely uninteresting, however – there's no point giving them a specific name. Martin-Löf type theories are defined to have some noncontractible base type(s), e.g. $\mathbb N$, $\mathbb B$ or $0$. Jan 23, 2021 at 13:58