coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type:Type and turning of universe consistency check

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Erik Palmgren <palmgren AT math.su.se>, Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: Re: [Coq-Club] Type:Type and turning of universe consistency check
Date: Sun, 12 Apr 2015 18:52:38 -0400

If you install UniMath (https://github.com/UniMath), it comes with a patched
version of Coq that has Type:Type.

Vladimir.

> On Apr 12, 2015, at 3:02 PM, Erik Palmgren
> <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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

RE: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Soegtrop, Michael, 04/01/2015
- Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/01/2015
  - RE: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Soegtrop, Michael, 04/02/2015
    - Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/02/2015
      - Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/02/2015
        
        Re: [Coq-Club] Term classification in ltac: has_var / is_constr / term complexity measure, Jonathan Leivent, 04/04/2015
      - [Coq-Club] Type:Type and turning of universe consistency check, Erik Palmgren, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Jason Gross, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Erik Palmgren, 04/12/2015
        
        Re: [Coq-Club] Type:Type and turning of universe consistency check, Vladimir Voevodsky, 04/13/2015