<p>The purpose of the system described in the appendix of the HoTT book is to present something that corresponds to what is used by the book. The book is aiming to be educational. Therefore it would be a bad idea to do everything in a minimalist way. For example, we introduce $\mathbb{N}$ separately because it is instructional to see how inductive constructions work in a familiar case.</p>

<p>You are perfectly correct, to jump-start inductive types from general $W$-types you just need $0$ and $2$. You immediately get $1$ as $0 \to 0$, and you get $+$ from $2$ and $\Sigma$. Once you have that, you get all finite sums $1 + 1 + \cdots + 1$. At this point it is easy to do the usual algebraic datatypes.</p>

<p>If you drop $0$, so you start from $\Pi$, $\Sigma$, $1$ and $2$, then you cannot get $0$ back because every type you make will be inhabited.</p>

<p>Suppose you only have $\Pi$, $\Sigma$, $0$ and $1$. Then you cannot make $2$ because you can show that every construction you make gives you back either $0$ or $1$. In fact, you cannot make any interesting dependent families at all. A larger family of types which is closed under $\Pi$, $\Sigma$, $0$ and $1$, but does not contain $2$ is the $(-1)$-types (propositions).</p>

CC BY-SA 3.0
2014-11-10T13:40:03.610Z
Okay, thanks for the answer. I suppose ${\bf 1}\equiv({\bf 0}\to {\bf 0})$ is possible in that framework due to $(\lambda x.x):({\bf 0}\to {\bf 0})$ being possible per definition of $\Pi$. Albeit that function $\lambda x.x$ which will never take an argument is awkward.
Nikolaj-K
CC BY-SA 3.0
2014-11-10T14:45:03.263Z
It might be useful to add that $W$-types present some technical caveats in the intentional theory: see e.g. [Observational Equality, Now!](http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf). Some (all?) of these are absent when the Univalence axiom is present.
cody
CC BY-SA 3.0
2016-04-07T18:26:58.077Z
I was thinking again about this question today. Actually, when we ware speaking of MLTT or HOTT, we also have equality for all types, I suppose, so we can get ${\bf 0}$ and ${\bf 1}=_U{\bf 2}$, right?
Nikolaj-K
CC BY-SA 3.0
2016-04-08T08:40:11.110Z
You could get $0$ that way, but note that $1 =_U 2$ refers to a universe $U$. And the $0$ so defined lives, awkwardly, in the next universe.
Andrej Bauer
CC BY-SA 3.0
2017-12-14T19:54:50.067Z
I am confused by "If you drop $0$, so you start from $\Pi$, $\Sigma$, $1$ and $2$, then you cannot get $0$ back because every type you make will be inhabited."  Since it is possible to construct empty types in pure calculus of constructions, which has only  $\Pi$.
user833970
CC BY-SA 4.0
2021-03-27T14:40:55.687Z
To answer both comments at once: the question was asked within the context of HoTT and MLTT. If you start switching things around (introduce an impredicative universe, like in the calculus of constructions) or removing function extensionality, then of course things can change. Why would that warrant a comment?
Andrej Bauer
CC BY-SA 3.0
2014-11-10T11:32:11.117Z
2014-11-10T11:32:11.117Z
Andrej Bauer
<p>I'm reading the formal presentation of <a href="http://en.wikipedia.org/wiki/Martin-L%C3%B6f_type_theory">Martin-Löfs type theory</a> (appendix of the <a href="http://homotopytypetheory.org/book/">HoTT book</a>). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also <a href="http://mazzo.li/epilogue/index.html%3Fp=324.html">$W$-types</a> as well as natural numbers $\mathbb N$ (inductively via $0$ and $succ$). Eventually they add <a href="http://ncatlab.org/nlab/show/higher+inductive+type">higher</a> inductive types too.</p>

<p>But then I wonder why it's necessary to do $\mathbb N$ in the theory specification. Doesn't ${\bf 1}$ and $+$ and <a href="http://en.wikipedia.org/wiki/Algebraic_data_type">algebraic</a> data types, in the incarnation of having $W$-types, suffice to set it up? E.g. with the <a href="http://en.wikipedia.org/wiki/F-algebra#Reccurence">initial algebra</a> approach. (Or at least after we pass from MLTT to HoTT have inductive types - after all, the integers $\mathbb Z$ emerge as <a href="http://en.wikipedia.org/wiki/Homotopy_group">homotopy group</a> of circle type $\mathbb S$ within the theory.)</p>

<p>Or has it to do with our need to have primitive recursion from the start, which is defined right next to $\mathbb N$ in the presentation? This is an idea which I have because I don't quite know how "definition is defined" in that framework, or how extending the language works, formally. I might add that I recognize that at least an informal notion of numbers and "greater" is used already when the hierarchy of universes is defined.</p>

<p>In case one can spare $\mathbb N$ and the specification is just not minimal, are there other items one could, in principle, drop? E.g. I could imagine $\bf 2$ and then $+$ coming from some combination of $\Pi, \Sigma, {\bf 0}, {\bf 1}$, but I was not able to do it.</p>

<type-theory>
Minimal specification of Martin-Löf type theory
Nikolaj-K
# Minimal specification of Martin-Löf type theory

(Asked by: username_0 on 2014-11-09)

I'm reading the formal presentation of [Martin-Löfs type theory](http://en.wikipedia.org/wiki/Martin-L%C3%B6f_type_theory) (appendix of the [HoTT book](http://homotopytypetheory.org/book/)). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also [$W$-types](http://mazzo.li/epilogue/index.html%3Fp=324.html) as well as natural numbers $\mathbb N$ (inductively via $0$ and $succ$). Eventually they add [higher](http://ncatlab.org/nlab/show/higher+inductive+type) inductive types too.

But then I wonder why it's necessary to do $\mathbb N$ in the theory specification. Doesn't ${\bf 1}$ and $+$ and [algebraic](http://en.wikipedia.org/wiki/Algebraic_data_type) data types, in the incarnation of having $W$-types, suffice to set it up? E.g. with the [initial algebra](http://en.wikipedia.org/wiki/F-algebra#Reccurence) approach. (Or at least after we pass from MLTT to HoTT have inductive types - after all, the integers $\mathbb Z$ emerge as [homotopy group](http://en.wikipedia.org/wiki/Homotopy_group) of circle type $\mathbb S$ within the theory.)

Or has it to do with our need to have primitive recursion from the start, which is defined right next to $\mathbb N$ in the presentation? This is an idea which I have because I don't quite know how "definition is defined" in that framework, or how extending the language works, formally. I might add that I recognize that at least an informal notion of numbers and "greater" is used already when the hierarchy of universes is defined.

In case one can spare $\mathbb N$ and the specification is just not minimal, are there other items one could, in principle, drop? E.g. I could imagine $\bf 2$ and then $+$ coming from some combination of $\Pi, \Sigma, {\bf 0}, {\bf 1}$, but I was not able to do it.

**Tags:** type-theory


---

## 1 answers

### Answer by username_1 on 2014-11-10. Score: 14 | Accepted answer

The purpose of the system described in the appendix of the HoTT book is to present something that corresponds to what is used by the book. The book is aiming to be educational. Therefore it would be a bad idea to do everything in a minimalist way. For example, we introduce $\mathbb{N}$ separately because it is instructional to see how inductive constructions work in a familiar case.

You are perfectly correct, to jump-start inductive types from general $W$-types you just need $0$ and $2$. You immediately get $1$ as $0 \to 0$, and you get $+$ from $2$ and $\Sigma$. Once you have that, you get all finite sums $1 + 1 + \cdots + 1$. At this point it is easy to do the usual algebraic datatypes.

If you drop $0$, so you start from $\Pi$, $\Sigma$, $1$ and $2$, then you cannot get $0$ back because every type you make will be inhabited.

Suppose you only have $\Pi$, $\Sigma$, $0$ and $1$. Then you cannot make $2$ because you can show that every construction you make gives you back either $0$ or $1$. In fact, you cannot make any interesting dependent families at all. A larger family of types which is closed under $\Pi$, $\Sigma$, $0$ and $1$, but does not contain $2$ is the $(-1)$-types (propositions).

> **Comments:**
> **username_0**: Okay, thanks for the answer. I suppose ${\bf 1}\equiv({\bf 0}\to {\bf 0})$ is possible in that framework due to $(\lambda x.x):({\bf 0}\to {\bf 0})$ being possible per definition of $\Pi$. Albeit that function $\lambda x.x$ which will never take an argument is awkward.  
> **username_2**: It might be useful to add that $W$-types present some technical caveats in the intentional theory: see e.g. [Observational Equality, Now!](http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf). Some (all?) of these are absent when the Univalence axiom is present.  
> **username_0**: I was thinking again about this question today. Actually, when we ware speaking of MLTT or HOTT, we also have equality for all types, I suppose, so we can get ${\bf 0}$ and ${\bf 1}=_U{\bf 2}$, right?  
> **username_1**: You could get $0$ that way, but note that $1 =_U 2$ refers to a universe $U$. And the $0$ so defined lives, awkwardly, in the next universe.  
> **username_3**: I am confused by "If you drop $0$, so you start from $\Pi$, $\Sigma$, $1$ and $2$, then you cannot get $0$ back because every type you make will be inhabited."  Since it is possible to construct empty types in pure calculus of constructions, which has only  $\Pi$.  
> **username_1**: To answer both comments at once: the question was asked within the context of HoTT and MLTT. If you start switching things around (introduce an impredicative universe, like in the calculus of constructions) or removing function extensionality, then of course things can change. Why would that warrant a comment?  

---

