In the Hott book, are the most of the type formers redundant? And if so, why? 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&#246;f type theory , https://cs.stackexchange.com/questions/82810/reducing-products-in-hott-to-church-scott-encodings/82891#82891
You are asking several questions which are similar but distinct. 


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 &lt; 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!) 
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.