The Coq mailing list

[Erik Palmgren <palmgren AT math.su.se>]

Thanks! That should be enough for the first experiemnts.

Erik

Jason Gross skrev den 2015-04-12 21:18:
> Coq 8.5 (beta) has -type-in-type (listed under coqc --help).  If you
> don't want to move to Coq 8.5, the closest you can get in Coq 8.4 is
> -impredicative-set, which doesn't quite give you what you want.  I think
> Vladimir Voevodsky and Dan Grayson also had a patch for Coq 8.4 that
> gave you Type:Type (but you have to build Coq from source, then, anyway).
>
> -Jason
>
> On Sun, Apr 12, 2015 at 3:02 PM, Erik Palmgren 
> <palmgren AT math.su.se
> <mailto:palmgren AT math.su.se>>
>  wrote:
>
>     Hello
>
>     I would like to experiment with computational behaviour in a type
>     theory with Type:Type. Is there any possibility to turn off universe
>     consistency check in (recent versions of) Coq? At same time I would
>     like to force Type(1):Type(1) (say).
>
>     I seem to remember experiments like this were indeed possible in old
>     Agda by simply making a suitable inductive-recursive definition of
>     such a universe and ignoring warnings of non-well foundedness.
>
>     Thanks
>
>     Erik Palmgren