The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

On Sat, Apr 30, 2011 at 4:35 AM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> It's just that "existT ... (projT1 a) (projT2 a)" is not convertible to
> "a" unless "a" is itself of the form "existT ... x y". Just make it so:

In case a longer-winded reply would also be helpful, here are some
thoughts from another homotopy theorist (and which will probably draw
a further correction from a type theorist or three).  I also find it
very tempting to think of { x:X & P x } as "the type of pairs (x,y)
such that x:X and y:P x", but doing so invariably gets me into
trouble.  When this happens, I find it helpful to remind myself that
actually, by definition, { x:X & P x } is only *inductively generated*
by pairs (x,y) such that x:X and y:P x.  That this can be a nontrivial
distinction in general is shown by the identity (= path) types
themselves, which are inductively generated by reflexivity proofs
alone, but which can nevertheless (in groupoid and homotopy models)
contain elements other than reflexivity proofs, that "come along for
the ride."

Dependent sum types differ from identity types, of course, in that we
can actually prove that everything in them is, at least up to
*propositional equality* (i.e. related by a path to), one of the
inductively generating elements (x,y).  This is essentially what your
lemma says.  But in order to prove that, we need to use the fact that
to prove something about a element of an inductive type, it suffices
to prove it in the case when the element is one of the generators.
This is why adding "destruct a" solves the problem.

Mike