What Comes After Sum Types?

Question

According to the first chapter of the HoTT book, dependent functions beget products:

$$ (x : A) \rightarrow B\,x \equiv: \prod_{x : A} B\,x $$

of which $A \times B$ is a special form ($A \times B \cong \prod_{b : \mathrm{Bool}} T\,b, T\,\mathrm{false} = A, T\,\mathrm{true} = B$),

and likewise, dependent products beget sums:

$$ (x : A) \times B\,x \equiv: \sum_{x : A} B\,x $$

of which $A + B$ is a special form.

I'm curious about the generalization of this scheme in both directions: What comes before $\rightarrow$ and after $+$ (and, possibly, so on) and how many inhabitants would these types have?

$(x : A) + B\,x$ is difficult for me to wrap my head around, since it seems to allow dependencies across alternative executions of a program. It also appears to be the case that in order to answer my question about how many elements inhabit this type, one must first describe an operation that lies beyond addition.

Answer 1

Let me propose a way to make your question precise. Let $\mathcal{U}$ be a universe.

Given a type former $X : (A : \mathcal{U}) \to (B : A \to \mathcal{U}) \to \mathcal{U}$ (like $\Sigma$ or $\Pi$), we can specialise it to a non-dependent binary type operator $\mathcal{U} \to \mathcal{U} \to \mathcal{U}$ in two ways:

• By letting $B$ be a constant type family, we get $X'\ A\ B := X\ A\ (\lambda a. B)$.
• By letting $A$ be a two-element type, we get $X^\mathbf{2}\ A\ B := X\ \mathbf{2}\ (\mathrm{rec}_\mathbf{2}^\mathcal{U}\ A\ B)$.

This explains how $\Sigma$-types generalise both sums and products ($\Sigma' = - \times -$ and $\Sigma^\mathbf{2} = - + -$) and $\Pi$-types generalise both products and functions ($\Pi' = - \to -$ and $\Pi^\mathbf{2} = - \times -$), leading to the confusing term "dependent product" being used to refer to both (see this question, this one, that one, this Twitter thread, etc.).

Your question is then: are there type formers $X$ and $Y$, definable in plain Martin-Löf type theory, such that $X' = - + -$ and $Y^\mathbf{2} = - \to -$?

We can answer both parts of the question negatively:

• Assume $X$ exists. Assuming function extensionality, any two functions $\mathbf{0} \to \mathcal{U}$ out of the empty type are equal. Thus we have $\mathbf{0} + \mathbf{1} = X\ \mathbf{0}\ (\lambda z. \mathbf{1}) = X\ \mathbf{0}\ (\lambda z. \mathbf{0}) = \mathbf{0} + \mathbf{0}$, but one of these types is inhabited and the other isn't.
• Assume $Y$ exists. Assuming univalence, there is an identification $\mathbf{2} = \mathbf{2}$ that swaps the two elements, so we have $(\mathbf{0} \to \mathbf{1}) = Y\ \mathbf{2}\ (\mathrm{rec}_\mathbf{2}^\mathcal{U}\ \mathbf{0}\ \mathbf{1}) = Y\ \mathbf{2}\ (\mathrm{rec}_\mathbf{2}^\mathcal{U}\ \mathbf{1}\ \mathbf{0}) = (\mathbf{1} \to \mathbf{0})$, but one of these types is inhabited and the other isn't.

Since MLTT is compatible with function extensionality and univalence, such a type former cannot be defined without further postulates.

Even if you allow postulating these things, I am not aware of any work in that direction. $\Sigma$ and $\Pi$ are useful because of their universal properties: in the categorical semantics of type theory, they are the left and right adjoint, respectively, to the base change functor that takes a type in context $\Gamma$ to a type in context $\Gamma. A$. It's a bit of a nice coincidence that both of these things can be specialised to yield binary products. By contrast, it isn't clear what universal property $X$ or $Y$ should satisfy.