# Can I have a "dependent coproduct type"?

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?

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.

• Hello. May I ask how you can show "$\sum$ and $\prod$ are left and right adjoint to substitiution."? What categories would be used? Jan 2, 2020 at 14:07
• I guess that the substitution is something like a diagonal functor and $A$ works as the index category of it. Then, maybe the category presumed is the category of types. Jan 3, 2020 at 3:13

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".