Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dependent Sums and Equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent Sums and Equality


chronological Thread 
  • From: Michael Shulman <mshulman AT ucsd.edu>
  • To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • Cc: ericfinster AT gmail.com, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Dependent Sums and Equality
  • Date: Sat, 30 Apr 2011 17:48:38 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=Bk4h/4qBdn4nH0scm4XF70YHc9rPtgMsEJDxcQAdd7dTDEzkXjCcKFwRKkFArXhpta 9Ra96M4qyQ3JuBecT6mKcavtyhYfntgIqbruXcEGLSqpeQGWe5ESCXx9OfXYsl5uGuFv btZKaetjAUUX134lqyplhgfUGI2pDhkS6tLMw=

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



Archive powered by MhonArc 2.6.16.

Top of Page