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