The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Good, so you quickly reconstructed the counterexample that I new to 
exist somewhere!

The additional ingredient to non-strict positivity you needed is a 
second universe above the impredicative one, and you have to place the 
non-strictly positive definition into that second higher universe.

However, this does not exclude non-strictly positive types in Prop.

* Since clever people like Chung-Kil can get them through the back door 
anyway, why not allow them outright?

* I'd bet that the proof-irrelevant set-theoretical model of Werner and 
Lee does support non-strictly positive types in Prop.

* I conjecture realizability models also support them.

Cheers,
Andreas

On 20.01.12 10:55 PM, Daniel Schepler wrote:
> Actually, I guess that also gives an example of a positive, but not
> strictly positive, inductive definition which would lead to a contradiction:
>
> Inductive X : Type :=
> | X_const : ((X->Prop)->Prop) -> X.
>
> If Coq allowed that definition, then X_const, being a constructor, would
> automatically be injective, leading to the contradiction from my
> previous message.  (Plus, I'm not at all sure what X_rect or X_ind would
> look like in that case.)
> --
> Daniel Schepler

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/