Can I have a "dependent coproduct type"?

Question

I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one.

The chapter introduces the function type $$ f:A\to B $$ and then generalizes it by making $B$ dependent on $x:A$ $$B:A\to\mathcal{U},\qquad g:\prod_{x:A}B(x)$$ and that is called the dependent function type.

Moving on, the chapter then introduces the product type $$ f:A\times B$$ and then generalizes it by making $B$ dependent on $x:A$ $$B:A\to\mathcal{U},\qquad g:\sum_{x:A}B(x)$$ and that is called the dependent pair type.

I can definitely see a pattern here.

Moving on, the chapter then introduces the coproduct type $$ f:A+B$$ and ... combobreaker ... there is no discussion of dependent version of this type.

Is there some fundamental restriction on that or it is just irrelevant for the topic of the book? In any case can someone help me with intuition on why function and product types? What makes those two so special that they get to be generalized to dependent types and then used to build up everything else?

Answer 1

The dependent sum is a common generalization of both the cartesian product $A \times B$ and the coproduct $A + B$. It just so happens that the HoTT book introduces dependent sum by generalizing $A \times B$, because that does not require the boolean type to be defined first.

The coproduct is a special case of dependent sum. Given types $A$ and $B$, consider the type family $P : \mathtt{bool} \to \mathcal{U}$ defined by $P(\mathtt{false}) = A$ and $P(\mathtt{true}) = B$. The dependent sum $\sum_{b : \mathtt{bool}} P(b)$ is equivalent to $A + B$. By the way, you can also get $A \times B$ as a dependent product $\prod_{b : \mathtt{bool}} P(b)$.

You ask what is special about products and function types. There are many, many reasons why $\sum$ and $\prod$ are "necessary". In terms of logic, they are necessary because they correspond to $\exists$ and $\forall$ by the propositions-as-types correspondence (but that only shifts the question to "why are $\exists$ and $\forall$ necessary?"). In terms of category theory, $\sum$ and $\prod$ are necessary because they are the left and right adjoint to substitution. Ask a more secific question if you would like to know more.

Answer 2

I'll talk about this more software-engineering-ly.

Are you talking about a coproduct type whose latter constructors can refer to prior ones (which, looks pretty similar to a product whose latter fields can refer to prior ones)? This is possible in Agda after HIT is introduced (in version 2.6.0):

-- Auxiliary definition: Nat
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- The HIT I was talking about
data Int : Set where
  positive : Nat -> Int
  negative : Nat -> Int
  -- Note this constructor uses `positive` and `negative`.
  zeroPath : positive zero ≡ negative zero

By following this paper, if your type-checker checks definitions defined using the syntax presented in figure "(26)", I believe it's quite simple to support "dependent coproducts".