# Tag Info

Accepted

• 31.7k
Accepted

### Dependent Sums and Products

I think what's confusing you is that $A \times B$ is both a product and a coproduct: It is the product of two factors, namely $A$ and $B$. It is the coproduct of $A$-many copies of $B$. Once you ...
• 26.7k

### In the Hott book, are the most of the type formers redundant? And if so, why?

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 ...
• 31.7k
Accepted

### Dependent Types and Compile Time Types

A language can be thought of as having both a static semantics, which determines the compile-time analysis that occurs; and a dynamic semantics, which determines the execution-time behavior of ...
• 266
Accepted

### In the Hott book, are the most of the type formers redundant? And if so, why?

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 ...
• 26.7k
Accepted

### Defining inductive types in intensional type theory purely in terms of type-theoretic data

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types ...
Accepted

### Reference for the fact that (0=1) implies false requires a universe in MLTT

I know of: Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.
Accepted

### Relating univalence for a theory of cateogries to the skeleton concept

I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't ...
• 26.7k