[Solved]: Can I have a "dependent coproduct type"?

Problem Detail: 

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?

Asked By : Kostya

Answered By : Andrej Bauer

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/28590

3.2K people like this

 Download Related Notes/Documents