<p>You are asking several questions which are similar but distinct. </p>

<ol>
<li><p>Why doesn't the HoTT book use Church encodings for data types?</p>

<p>Church encodings do not work in Martin-Löf type theory, for two reasons. </p>

<p>First, MLTT is <em>predicative</em>. There is a universe hierarchy, and each type lives at a particular universe level, and a type at level $n$ can only quantify over types at smaller universe levels $k &lt; n$. Church encodings like in System F or the CoC require <em>impredicative</em> quantification, where you can instantiate quantifiers with types which are the same size, or even bigger. </p>

<p>Second, even if you defined datatypes like the natural numbers with Church encodings, to do proofs with these types, you need <em>induction principles</em> to prove things about them. To derive induction principles for Church encodings, you need to use an argument based on Reynolds' parametricity, and the question of how to internalize parametricity principles into type theory is still not fully settled. (The state of the art is Nuyts, Vezzosi, and Devriese's ICFP 2017 paper <em>Parametric Quantifiers for Dependent Type Theory</em> -- note that this is well <em>after</em> the HoTT book was written!) </p></li>
<li><p>Next, you are asking why the foundation is not minimal. This is actually one of the distinctive sociological features of type-theoretic foundations -- type theorists regard having a small set of rules as a technical convenience, without much foundational significance. It's far, far more important to have the <em>right</em> set of rules, rather than the <em>smallest</em> set of rules. </p>

<p>We develop type theories to be <strong>used</strong> by mathematicians and programmers, and it's very, very important that the proofs done within type theory are the ones that mathematicians and programmers regard as being done in the right way. This is because the arguments mathematicians typically regard as having good style typically are structured using the key algebraic and geometrical principles of the domain of study. If you have to use complicated encodings then much structure is lost or obscured. </p>

<p>This is why even type-theoretic presentations of propositional classical logic invariably give all the logical connectives, even though it is formally equivalent to a logic with just NAND. Sure, all the boolean connectives can be encoded with NAND, but that encoding obscures the structure of the logic. </p></li>
</ol>

CC BY-SA 3.0
2017-12-15T13:09:23.043Z
Thanks for this answer! I'll need to read that paper (and yours) and it might make more sense.  But, I thought the universe hierarchy was designed to make it look like you can do predicative things: for instance (λA:U.λa:A.a)(ΠA:U.A→A) would desugar to (λA:Un+1.λa:A.a)(ΠA:Un.A→A).

I do think that it is a strange editorial choice not to explain this, every logic book I know points out several more minimal encoding like CNF, DNF, NAND and so on.  And anyone who is used to set theory expects a "natural" encoding of the Nats, to demonstrate the theory.  But that may just be my classical biases.
user833970
CC BY-SA 3.0
2017-12-15T13:28:44.447Z
that should be "impredicative" in my last comment
user833970
CC BY-SA 3.0
2017-12-16T18:06:26.033Z
CNF, DNF, NAND and so on are irrelevant in this context, as they are about a tiny subset of logic, namely the Boolean part. They are useless in type theory (which isn't logic). As for your encodings, they won't work because they land in a universe one higher than we want it, and also they don't have the correct elimnation properties. The type $\prod (T : U_n) . T$ is "empty" only as far as $U_n$ is concerned (what do other universes think about it?), and it lands in $U_{n+1}$ instead of $U_n$.
Andrej Bauer
CC BY-SA 3.0
2017-12-16T21:28:24.190Z
Perhaps I am misunderstanding something about universe hierarchies.  I thought that we never care which specific Universe a type is in, only that the universe numbers can be assigned when we want to verify a proof.  So technically ΠT:U.T is a family of types indexed over universes.  Just like the polymorphic identity is a family of types indexed over universes. But don't we have the same problem with the polymorphic identity?  I'd really appreciate it if you could expand on the last 2 sentences, I don't think I understand.
user833970
CC BY-SA 3.0
2017-12-16T21:32:40.137Z
When you say that it doesn't have the right elimination properties do you mean that once the universe is fixed there are types in higher universes that cannot be directly synthesized by a term of ΠT:Un.T?
user833970
CC BY-SA 3.0
2017-12-17T13:04:56.980Z
I explained the difficulties in a separate answer.
Andrej Bauer
CC BY-SA 3.0
2017-12-20T15:54:29.880Z
This is still a really good answer, but I'm moving the check mark to  Andrej's answer because it deals with the specifics of my "encoding".  I wish I could accept both.
user833970
CC BY-SA 3.0
2017-12-15T10:28:58.233Z
2017-12-15T10:28:58.233Z
Neel Krishnaswami
<p>Let me explain why the suggested encoding of the empty type does not work. We need to be explicit about universe levels and not sweep them under the rug.</p>

<p>When people say "the empty type", they might mean one of two things:</p>

<ol>
<li><p>A <em>single</em> type $E$ which is empty with respect to all types. Such a type has the elimination rule: for every $n$ and type family $A : E \to U_n$, there is a map $e_{n,A} : E \to A$.</p></li>
<li><p>A family of types $E_k$, one for each universe level $k$, such that $E_k$ is "the empty type of $U_k$". Such a type has to satisfy $E_k : U_k$, obviously, and also: for every type family $A : E_{k} \to U_k$, there is a map $e_{k,A} : E_{k} \to A$.</p></li>
</ol>

<p>Without any provisos, when people say "empty type" they expect the first meaning above. </p>

<p>How can we get $E$? A first try could be something like
$$E = \Pi (T : U) \,.\, T$$
but this is precisely the sort of sweeping under the rug that creates confusion. We must write down explicit universe levels. If we write something like
$$E_k = \Pi (T : U_k) \,.\, T$$
then we get a sequence of types $E_0, E_1, E_2, \ldots$, one for each level $k$. We might hope that this sequence is the empty type in the sense above, but it is not, because $E_k$ is in $U_{k+1}$ but it is supposed to be in $U_k$.</p>

<p>Another try is
$$E = \Pi n \,.\,\Pi (T : U_{n}) \,.\, T$$
but now you have to explain what "$\Pi n$" is supposed to be. You might be tempted to say that there is a type $L$ of universe levels, and so
$$E = \Pi (n : L) \,.\,\Pi (T : U_{n}) \,.\, T$$
You have now fallen into a trap, because I will ask: in which universe does $E$ live? And in which universe does $L$ live? This is not going to work.</p>

<p>There is a solution, known as <em>impredicative universe</em>. This is a magical universe $U$ which has the property that, given $B : U \to U$, the type $\Pi (X : U) B(X)$ lives in $U$ (and not one level up from $U$). Then at least $\Pi (X : U) X$ is again in $U$, and will have the expected eliminator. But we are still not done, as now we have to worry about equations for the eliminator, as was pointed out by Neel.</p>

<p>Impredicative universes can be arranged. However, a famous theorem of Thierry Coquand (if I am not mistaken), shows that having <em>two</em> impredicative universes, one contained in the other, leads to a contradiction.</p>

<p>The moral of the story is: just axiomatize the empty type directly and stop encoding things.</p>

CC BY-SA 3.0
2017-12-21T06:10:26.683Z
That is a convincing reasoning to axiomatize the empty type, but I'm still curious about the reasoning to axiomatize all those heavier things.
MaiaVictor
CC BY-SA 3.0
2017-12-21T20:40:42.983Z
@MaiaVictor: as opposed to what?
Andrej Bauer
CC BY-SA 3.0
2017-12-21T22:22:40.077Z
Sorry? I just mean you convincingly justified why it is a good idea to axiomatize the empty type in particular. But OP also asked about other things: *"universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, natural number type, and identity types"* (which I assume are also primitives on the system proposed on the HoTT book). (I'm obviously not asking you to justify those all, just manifesting my interest.)
MaiaVictor
CC BY-SA 4.0
2018-09-24T18:53:46.830Z
@MaiaVictor: The story with the other types is very similar. For instance, the unit type looks a bit like it could be encoded as $\mathbb{1} = \prod_{X : U} (X \to X)$; however problems arise as soon as one tries to be more precise with that definition.
Ingo Blechschmidt
CC BY-SA 4.0
2018-09-24T20:44:57.093Z
@IngoBlechschmidt curious to learn what kinds of problems! It looks good to me...
MaiaVictor
CC BY-SA 4.0
2018-09-25T21:48:12.287Z
@MaiaVictor: For instance that the type $\prod_{X : U} (X \to X)$ doesn't live in $U$, but in the next universe. Depending on what you want, this can be undesirable. Also it's not clear that every inhabitant of $\prod_{X : U} (X \to X)$ is actually equal to $\lambda (X : U). \lambda (x : X). x$.
Ingo Blechschmidt
CC BY-SA 3.0
2017-12-17T13:04:41.833Z
2017-12-20T00:04:52.833Z
2017-12-20T00:04:52.833Z
Andrej Bauer
<p>In chapter 1 and Appendix A of the <a href="https://homotopytypetheory.org/book/" rel="noreferrer">Hott book</a>, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, natural number type, and identity types) to form the foundation for Homotopy Type Theory.</p>

<p>However it seems that given universe types, and dependent function types you can construct all these other "primitive" types.  For instance the Empty type could instead be defined as </p>

<pre><code>ΠT:U.T
</code></pre>

<p>I assume the other types could also be constructed similar to how they are in <a href="https://en.wikipedia.org/wiki/Calculus_of_constructions#Defining_logical_operators" rel="noreferrer">pure CC</a>, (ie just derive the type from the inductive part of the definition).</p>

<p>Many of these types are explicitly made redundant by the Inductive/W types that are introduced in chapters 5 and 6.  But Inductive/W types appear to be an optional part of the theory since there are open questions on how they interact with HoTT (at least at the time the book came out).</p>

<p>So I am very confused about why these additional types are presented as primitive.  My intuition is that a foundational theory should be as minimal as possible, and redefining a redundant Empty type as a primitive into the theory seems very arbitrary.</p>

<p>Was this choice made</p>

<ul>
<li>for some some metatheoretic reasons that I am unaware of?</li>
<li>for historical reasons, to make the type theory look like
past type theories (which were not necessarily trying to be
foundational)?</li>
<li>for "usability" of computer interfaces?</li>
<li>for some advantage in proof search that I am unaware of?</li>
</ul>

<p>Similar to: <a href="https://cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-l%C3%B6f-type-theory?rq=1">Minimal specification of Martin-L&#246;f type theory</a> , <a href="https://cs.stackexchange.com/questions/82810/reducing-products-in-hott-to-church-scott-encodings/82891#82891">https://cs.stackexchange.com/questions/82810/reducing-products-in-hott-to-church-scott-encodings/82891#82891</a></p>

CC BY-SA 3.0
2017-12-16T18:09:26.303Z
They are redundant, but not in the way you're suggesting. You should ask yourself **what purpose** does "minimality of foundation" serve? And do we care about the purpose?
Andrej Bauer
CC BY-SA 3.0
2017-12-16T19:43:42.613Z
I assume technical work is minimal by convention, where things don't need to be minimal if it is obviously convenient or explicitly noted otherwise.  The book even adheres to this in other places, like when it defines truncation types (defined by rules, but explicitly not minimal).  For example if I saw the nats defined in terms of 0,1,10, the successor and the power operation, I would be confused, but I could at least see why it is notationally convenient.  Hott is a much more complex area of study and I want to know if I am missing anything obvious.
user833970
CC BY-SA 3.0
2017-12-16T19:47:34.383Z
I also have interest in computer implementation, but I think that is a bit more specific.
user833970
CC BY-SA 3.0
2017-12-17T12:44:58.073Z
For computer implementation you most definitely do not want to go minimal. You want to strike a good balance between *simplicity* and *expressivity*. But you also skipped my question when you said "assume technical work is minimal by convention". You should contemplate on such conventions and worry about them, especially when people do not know why they are there. There is a deeper issue here which touches on your question about the HoTT foundations. There are reasons we *don't want* the kind of minimalist foundation you are asking about. They are *harmful* in certain situations.
Andrej Bauer
CC BY-SA 3.0
2017-12-17T18:39:07.837Z
I would be very interested in hearing about how they can be harmful.  Should I make a new question about that?
user833970
CC BY-SA 3.0
2017-12-21T06:05:40.473Z
@AndrejBauer I'd like to know why they would be harmful, too. My reasoning to believe the foundational language should be minimal is the reasoning behind occam's razor, it is unjustified added complexity. Why stop there? Why not add also lists, strings, pairs, triples, vectors? Those seems arbitrary choices, what justifies them? Edit: I just noticed this question has answers; but I'll leave this comment here just for the sake of noting why I'd be interested in that too.
MaiaVictor
CC BY-SA 3.0
2017-12-21T20:41:04.210Z
I'll write a blog post.
Andrej Bauer
<type-theory><dependent-type><homotopy-type-theory>
In the Hott book, are the most of the type formers redundant? And if so, why?
user833970
# In the Hott book, are the most of the type formers redundant? And if so, why?

(Asked by: username_0 on 2017-12-14)

In chapter 1 and Appendix A of the Hott book, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, natural number type, and identity types) to form the foundation for Homotopy Type Theory.
However it seems that given universe types, and dependent function types you can construct all these other "primitive" types.  For instance the Empty type could instead be defined as 
ΠT:U.T

I assume the other types could also be constructed similar to how they are in pure CC, (ie just derive the type from the inductive part of the definition).
Many of these types are explicitly made redundant by the Inductive/W types that are introduced in chapters 5 and 6.  But Inductive/W types appear to be an optional part of the theory since there are open questions on how they interact with HoTT (at least at the time the book came out).
So I am very confused about why these additional types are presented as primitive.  My intuition is that a foundational theory should be as minimal as possible, and redefining a redundant Empty type as a primitive into the theory seems very arbitrary.
Was this choice made

for some some metatheoretic reasons that I am unaware of?
for historical reasons, to make the type theory look like
past type theories (which were not necessarily trying to be
foundational)?
for "usability" of computer interfaces?
for some advantage in proof search that I am unaware of?

Similar to: Minimal specification of Martin-Löf type theory , https://cs.stackexchange.com/questions/82810/reducing-products-in-hott-to-church-scott-encodings/82891#82891

**Tags:** type-theory, dependent-type, homotopy-type-theory

> **Comments:**
> **username_1**: They are redundant, but not in the way you're suggesting. You should ask yourself **what purpose** does "minimality of foundation" serve? And do we care about the purpose?  
> **username_0**: I assume technical work is minimal by convention, where things don't need to be minimal if it is obviously convenient or explicitly noted otherwise.  The book even adheres to this in other places, like when it defines truncation types (defined by rules, but explicitly not minimal).  For example if I saw the nats defined in terms of 0,1,10, the successor and the power operation, I would be confused, but I could at least see why it is notationally convenient.  Hott is a much more complex area of study and I want to know if I am missing anything obvious.  
> **username_0**: I also have interest in computer implementation, but I think that is a bit more specific.  
> **username_1**: For computer implementation you most definitely do not want to go minimal. You want to strike a good balance between *simplicity* and *expressivity*. But you also skipped my question when you said "assume technical work is minimal by convention". You should contemplate on such conventions and worry about them, especially when people do not know why they are there. There is a deeper issue here which touches on your question about the HoTT foundations. There are reasons we *don't want* the kind of minimalist foundation you are asking about. They are *harmful* in certain situations.  
> **username_0**: I would be very interested in hearing about how they can be harmful.  Should I make a new question about that?  
> **username_2**: @AndrejBauer I'd like to know why they would be harmful, too. My reasoning to believe the foundational language should be minimal is the reasoning behind occam's razor, it is unjustified added complexity. Why stop there? Why not add also lists, strings, pairs, triples, vectors? Those seems arbitrary choices, what justifies them? Edit: I just noticed this question has answers; but I'll leave this comment here just for the sake of noting why I'd be interested in that too.  
> **username_1**: I'll write a blog post.  

---

## 2 answers

### Answer by username_1 on 2017-12-17. Score: 15 | Accepted answer

Let me explain why the suggested encoding of the empty type does not work. We need to be explicit about universe levels and not sweep them under the rug.

When people say "the empty type", they might mean one of two things:

1. A *single* type $E$ which is empty with respect to all types. Such a type has the elimination rule: for every $n$ and type family $A : E \to U\_n$, there is a map $e\_{n,A} : E \to A$.
2. A family of types $E\_k$, one for each universe level $k$, such that $E\_k$ is "the empty type of $U\_k$". Such a type has to satisfy $E\_k : U\_k$, obviously, and also: for every type family $A : E\_{k} \to U\_k$, there is a map $e\_{k,A} : E\_{k} \to A$.

Without any provisos, when people say "empty type" they expect the first meaning above.

How can we get $E$? A first try could be something like
$$E = \Pi (T : U) \,.\, T$$
but this is precisely the sort of sweeping under the rug that creates confusion. We must write down explicit universe levels. If we write something like
$$E\_k = \Pi (T : U\_k) \,.\, T$$
then we get a sequence of types $E\_0, E\_1, E\_2, \ldots$, one for each level $k$. We might hope that this sequence is the empty type in the sense above, but it is not, because $E\_k$ is in $U\_{k+1}$ but it is supposed to be in $U\_k$.

Another try is
$$E = \Pi n \,.\,\Pi (T : U\_{n}) \,.\, T$$
but now you have to explain what "$\Pi n$" is supposed to be. You might be tempted to say that there is a type $L$ of universe levels, and so
$$E = \Pi (n : L) \,.\,\Pi (T : U\_{n}) \,.\, T$$
You have now fallen into a trap, because I will ask: in which universe does $E$ live? And in which universe does $L$ live? This is not going to work.

There is a solution, known as *impredicative universe*. This is a magical universe $U$ which has the property that, given $B : U \to U$, the type $\Pi (X : U) B(X)$ lives in $U$ (and not one level up from $U$). Then at least $\Pi (X : U) X$ is again in $U$, and will have the expected eliminator. But we are still not done, as now we have to worry about equations for the eliminator, as was pointed out by Neel.

Impredicative universes can be arranged. However, a famous theorem of Thierry Coquand (if I am not mistaken), shows that having *two* impredicative universes, one contained in the other, leads to a contradiction.

The moral of the story is: just axiomatize the empty type directly and stop encoding things.

> **Comments:**
> **username_2**: That is a convincing reasoning to axiomatize the empty type, but I'm still curious about the reasoning to axiomatize all those heavier things.  
> **username_1**: @username_2: as opposed to what?  
> **username_2**: Sorry? I just mean you convincingly justified why it is a good idea to axiomatize the empty type in particular. But OP also asked about other things: *"universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, natural number type, and identity types"* (which I assume are also primitives on the system proposed on the HoTT book). (I'm obviously not asking you to justify those all, just manifesting my interest.)  
> **username_4**: @username_2: The story with the other types is very similar. For instance, the unit type looks a bit like it could be encoded as $\mathbb{1} = \prod_{X : U} (X \to X)$; however problems arise as soon as one tries to be more precise with that definition.  
> **username_2**: @IngoBlechschmidt curious to learn what kinds of problems! It looks good to me...  
> **username_4**: @username_2: For instance that the type $\prod_{X : U} (X \to X)$ doesn't live in $U$, but in the next universe. Depending on what you want, this can be undesirable. Also it's not clear that every inhabitant of $\prod_{X : U} (X \to X)$ is actually equal to $\lambda (X : U). \lambda (x : X). x$.  

---

### Answer by username_3 on 2017-12-15. Score: 16

You are asking several questions which are similar but distinct.

1. Why doesn't the HoTT book use Church encodings for data types?

   Church encodings do not work in Martin-Löf type theory, for two reasons.

   First, MLTT is *predicative*. There is a universe hierarchy, and each type lives at a particular universe level, and a type at level $n$ can only quantify over types at smaller universe levels $k < n$. Church encodings like in System F or the CoC require *impredicative* quantification, where you can instantiate quantifiers with types which are the same size, or even bigger.

   Second, even if you defined datatypes like the natural numbers with Church encodings, to do proofs with these types, you need *induction principles* to prove things about them. To derive induction principles for Church encodings, you need to use an argument based on Reynolds' parametricity, and the question of how to internalize parametricity principles into type theory is still not fully settled. (The state of the art is Nuyts, Vezzosi, and Devriese's ICFP 2017 paper *Parametric Quantifiers for Dependent Type Theory* -- note that this is well *after* the HoTT book was written!)
2. Next, you are asking why the foundation is not minimal. This is actually one of the distinctive sociological features of type-theoretic foundations -- type theorists regard having a small set of rules as a technical convenience, without much foundational significance. It's far, far more important to have the *right* set of rules, rather than the *smallest* set of rules.

   We develop type theories to be **used** by mathematicians and programmers, and it's very, very important that the proofs done within type theory are the ones that mathematicians and programmers regard as being done in the right way. This is because the arguments mathematicians typically regard as having good style typically are structured using the key algebraic and geometrical principles of the domain of study. If you have to use complicated encodings then much structure is lost or obscured.

   This is why even type-theoretic presentations of propositional classical logic invariably give all the logical connectives, even though it is formally equivalent to a logic with just NAND. Sure, all the boolean connectives can be encoded with NAND, but that encoding obscures the structure of the logic.

> **Comments:**
> **username_0**: Thanks for this answer! I'll need to read that paper (and yours) and it might make more sense.  But, I thought the universe hierarchy was designed to make it look like you can do predicative things: for instance (λA:U.λa:A.a)(ΠA:U.A→A) would desugar to (λA:Un+1.λa:A.a)(ΠA:Un.A→A).  I do think that it is a strange editorial choice not to explain this, every logic book I know points out several more minimal encoding like CNF, DNF, NAND and so on.  And anyone who is used to set theory expects a "natural" encoding of the Nats, to demonstrate the theory.  But that may just be my classical biases.  
> **username_0**: that should be "impredicative" in my last comment  
> **username_1**: CNF, DNF, NAND and so on are irrelevant in this context, as they are about a tiny subset of logic, namely the Boolean part. They are useless in type theory (which isn't logic). As for your encodings, they won't work because they land in a universe one higher than we want it, and also they don't have the correct elimnation properties. The type $\prod (T : U_n) . T$ is "empty" only as far as $U_n$ is concerned (what do other universes think about it?), and it lands in $U_{n+1}$ instead of $U_n$.  
> **username_0**: Perhaps I am misunderstanding something about universe hierarchies.  I thought that we never care which specific Universe a type is in, only that the universe numbers can be assigned when we want to verify a proof.  So technically ΠT:U.T is a family of types indexed over universes.  Just like the polymorphic identity is a family of types indexed over universes. But don't we have the same problem with the polymorphic identity?  I'd really appreciate it if you could expand on the last 2 sentences, I don't think I understand.  
> **username_0**: When you say that it doesn't have the right elimination properties do you mean that once the universe is fixed there are types in higher universes that cannot be directly synthesized by a term of ΠT:Un.T?  
> **username_1**: I explained the difficulties in a separate answer.  
> **username_0**: This is still a really good answer, but I'm moving the check mark to  Andrej's answer because it deals with the specifics of my "encoding".  I wish I could accept both.  

---

