# Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the simply typed world. In an ML-like language we can encode existential types in terms of universal types:

$\exists a.T(a) \equiv \forall x.(\forall a.T(a) \rightarrow x) \rightarrow x$

Similarly, we could also define sum types in terms of universal types and product types:

$a + b \equiv \forall x.(a \rightarrow x)\times(b \rightarrow x) \rightarrow x$

This correspondence makes sense to me, since existential types are like infinite sums and universal types are like infinite products.

In a dependently typed language, would it also be possible to define dependent sums in terms of dependent products? This seems close:

$\Sigma(b:B).T(b) \equiv \forall x.(\Pi(b:B).T(b) \rightarrow x) \rightarrow x$

$(a,t) : \Sigma(b:B).T(b) \equiv \lambda f. f\ a\ t$

$\text{fst}\ p \equiv p_B\ (\lambda(b:B).\lambda(\_:T(b)).b)$

$\text{snd}\ p \equiv p_{T (\text{fst}\ p)}\ (\lambda(b:B).\lambda(t:T(b)).t)$

However, I can't convince myself that the definition for snd is well-typed because I can't show that $t : T (\text{fst}\ p)$. Is there some way to make this work?

-
See a Math.SE question: Is it possible to express sigma-type in Martin-Löf type theory with other constructs: math.stackexchange.com/questions/661511/… – fread2281 Aug 27 '14 at 15:56

My understanding is that dependent elimination cannot be derived from impredicative encodings, but I cannot find a reference other than a passing mention in The Implict Calculus of Constructions.

-
I'm given to understand that this is because you can't prove the universality of the impredicative encodings without parametricity (i.e., $\beta\eta$ isn't enough), and so of course the internal equality of the type theory isn't enough to prove the soundness of the strong elims. You might be able to define a universe with (some generalization of?) setoids where it does work, though. – Neel Krishnaswami Feb 26 '10 at 9:44

The statement "for any type-indexed family of propositions exists a proposition isomorphic to their coproduct" is inconsistent with impredicative type theory (CC); this leads to Girard's Paradox.

The statement "for any proposition-indexed family of propositions there exists a proposition isomorphic to their coproduct" is independent from impredicative type theory (CC). That is, CC has models in which this is false. For the proof, see T Streicher, Independence results for calculi of dependent types in Category Theory and Computer Science, 1989.

So, if what you're looking for were possible, I think it would have to include some sort of "gotcha" that made it incompatible with $B:Prop\ \&\ T:(B\to Prop)\Rightarrow(\Sigma b:B.T(b)):Prop$. I'd guess that this sort of gotcha (if it exists) would be something like requiring $(\Sigma b:B.T(b)):Type$ -- that dependent sums are one universe up from their coordinates.

As Russell mentions, Coq gets around this by using a stronger theory (CiC) from which the statement in the second paragraph is not independent.

-
There's a shift in kind between Keith's first and second examples: the dependent sum he gives is only indexed over a value, not a type. (I.e., $B$ is a type, not a kind.) So it's not immediately obvious that this leads to inconsistency, since you can support strong elims for small sums in CC without consistency problems. – Neel Krishnaswami Mar 1 '10 at 12:12

Have a look at hoq Coq defines dependent sums in terms of dependent products in the standard library. Specifically, you should look at http://coq.inria.fr/stdlib/Coq.Init.Specif.html.

-
Is that really "in terms of dependent products"? I thought Coq's dependent sums were defined as inductive types, not by simple formulas using only dependent products, which is what the question seems to be asking for. – Mike Shulman Feb 26 '10 at 1:48
Good point, of course if what Russell says is true, then something like an induction principle is needed to get things working. – Andrej Bauer Feb 26 '10 at 19:34

This is certainly not what the question was after, but since the answers seem to be something along the lines of yes, sometimes, but not unless...

Multi-sorted first-order logic (i.e., classical logic) can be considered a realisation of dependent type theory by enriching the universe of terms to contain enough structure to model the required inference rules, which are richer, because of De Morgan duality. Most crucially, you need Hilbert's epsilon operator to model the elimination rule for dependent sums. The resulting theory is nonconstructive —in a strong sense: the equivalence theory on terms is undecidable— but can be given a straightforward interpretation in ZFC. Dependent sum and product are then existential and universal quantification, so either can be encoded in terms of the others.

I haven't though carefully about this stuff in over ten years, but it is essentially the same as an observation due, IIRC, to Bill Tait, that ZFC set theory highlights a weakness of using the BHK interpretation to fix the notion of constructive logic - if the notion of construction is left uninterpreted, then ZFC provides a notion of "construction" upon which can be based a BHK interpretation of classical logic. Corollary: the BHK interpretation does not do the work that many people think it does.

-