Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] CiC without elim restriction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CiC without elim restriction


chronological Thread 
  • From: Dan Doel <dan.doel AT gmail.com>
  • To: Bruno Barras <bruno.barras AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] CiC without elim restriction
  • Date: Tue, 29 Nov 2011 11:39:02 -0500

On Tue, Nov 29, 2011 at 6:47 AM, Bruno Barras 
<bruno.barras AT inria.fr>
 wrote:
> I should have said "small sum in an impredicative sort". It's not always
> clear what the impredicative word applies to: is it each feature that is
> considered impredicative or not, or is it the whole theory ?

I think traditionally it's individual definitions that are
impredicative or not. A definition is impredicative if it makes
essential use of the (an?) entire collection containing the thing it
is defining. Or something close to that. You can then go on to label
features or theories as impredicative based on whether they admit such
definitions (and possibly, just how much self-reference you think is
ok before something becomes impredicative).

So, { S : Set & unit } : Set is impredicative because it's defining a
Set by quantifying over all Sets (which contains { S : Set & unit }),
but { n : nat & unit } : Set is arguably not, because Set is not
subsumed by nat, even if we (artificially) stick nat in a much higher
universe than Set. It's the same rule that allows both, but the rule
is labelled impredicative because it allows the impredicative
definition, not because all definitions that make use of it are
impredicative.

At least, that's my take on the matter as of now.

> What is clear to me is that the impredicative product types of Set have a
> global impact on the theory. For instance it is incompatible with
> interpreting each predicative product (in Type) as the set of set-theoretic
> functions (that's the Chicli-Pottier-Simpson paradox).

Yeah, it has a few not-so-obvious consequences. For instance, I
believe it's also incompatible with the injectivity of type
constructors, which almost seems like a sensible thing to have from a
purely syntactic perspective.

-- Dan



Archive powered by MhonArc 2.6.16.

Top of Page