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?