0
$\begingroup$

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

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Jan 23, 2021 at 8:05
  • $\begingroup$ 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$. $\endgroup$
    – varkor
    Jan 23, 2021 at 13:58

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy