<p>If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example <span class="math-container">$0:\mathbb{N}$</span> is constructed when defining <span class="math-container">$\mathbb{N}$</span> and does not reduce to anything else.</p>
<p>But if we are in a pure Martin-Löf type theory then any inhabitant of any type ultimately refers to <span class="math-container">$*:\mathbf{1}$</span>. Is there a name for this property (akin to normalization/canonicity)?</p>

CC BY-SA 4.0
2021-01-23T08:05:18.600Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-01-23T13:58:28.243Z
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$.
varkor
<type-theory><coq><calculus-of-constructions>
What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?
tts
# What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?

(Asked by: username_0 on 2021-01-23)

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)?

**Tags:** type-theory, coq, calculus-of-constructions
> **Comments:**
> **username_1**: 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.  
> **username_2**: 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$.  

---

## 0 answers

