Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
2  
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

1 Answer 1

up vote 5 down vote accepted

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

share|improve this answer
    
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
    
So the section immediately following dependent sums discusses coproduct types, which answers my first question. I'm still curious as to the nature of superexponential types. Are they inhabited by functions of multiple variables? –  Nate Aug 3 '13 at 20:43
    
That's taking the arithmetic analogy rather too far, I think! –  Zhen Lin Aug 3 '13 at 20:57

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.