# Confusion about Homotopy Type Theory terminology

I've picked up the Homotopy Type Theory book for leisure. I'm comfortable with strongly typed languages and familiar with dependently typed languages and I enjoy topology, so I thought that the HoTT book was a good opportunity to learn some of the math underlying the type systems (and, by HoTT's reputation, a new way of looking at many other things I know.)

I'd dabbled a bit in formal type theory previous to HoTT. I've long thought of (independent) types like this:

Unit data types are types with only one value, isomorphic to:

data Unity = Unity


You can sum types, creating a type inhabited by as many values as A + B

data Sum a b = Left a | Right b


more commonly known as Either a b in programming circles.

Then there are product types, which house as many types as A × B

data Product a b = Both a b


more commonly known as (a, b).

Finally there are exponential types inhabited by as many values as there are mappings A → B (which is $B^A$). These are more commonly known as functions, and defining them is my day job. The little algebraic type theory I know is founded in those assumptions. (I'm curious what's beyond exponential types in this progression, but that's besides the point.)

The HoTT book starts out by defining the exponential type $\rightarrow$, the dependent function type $\Pi$, the product type $\times$, and the dependent pair type $\Sigma$. The definitions all make sense, but I find the naming confusing. Function types seem pretty exponential to me: why are dependent function types (a generalization of $\rightarrow$) denoted $\Pi$ ('product')?

This doesn't seem like just a silly mistake: the product type $\times$ is generalized to a dependent product type $\Sigma$ ('summation').

Both types are "demoted" when they're generalized (exponential to product, product to sum). There's obviously some reasoning behind this naming, but it's going right over my head.

Why does Homotopy Type Theory use this naming scheme? What's the isomorphism that I'm missing?

-
This is standard in dependent type theory, and is rooted in mathematics: after all, what is $X \times Y$ if not the sum of $X$-many copies of $Y$? – Zhen Lin Aug 3 '13 at 19:53
Oh. Neat. I feel silly now. Want to write that up as an answer? – Nate Aug 3 '13 at 19:57

The usual names for $\Sigma$-types and $\Pi$-types are dependent sum and dependent product, respectively, but for some reason the Homotopy Type Theory book calls them dependent pair type and dependent function type.
Whatever you call them, they respectively generalise binary products and exponentiation: $X \times Y$ is just the sum of $X$-many copies of $Y$, i.e. $\sum_{x : X} Y$, and $Y^X$ is the product of $X$-many copies of $Y$, i.e. $\prod_{x : X} Y$.
Neat. I suppose you could go a step further and say that there's a Successor type data Succ a = Zero | Succ a (known as Maybe to programmers), and then generalize sum types $A + B$ as dependent succession $Succ_{x:A} B$, and then generalize Succession as dependent unity and complete the pattern. Out of curiosity, what do you call independent types that generalize into dependent exponents (i.e. superexponential types), and what would they look like? – Nate Aug 3 '13 at 20:30
I think the reason the book calls them "dependent pair" and "dependent function" is exactly the confusion evidenced in this question: $\Sigma$-types generalize both binary sum types (by $\Sigma$-ing over Bool) and binary product types (when $Y$ is independent of $X$), so it may not be clear whether it should be called the "dependent sum" or the "dependent product". (And indeed, I've heard that the occasional person actually does call $\Sigma$ a "dependent product".) – Mike Shulman Nov 5 '14 at 5:53