Can dependent sums be encoded as dependent products?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.