coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tarski style universes in Coq

From: Bas Spitters <spitters AT cs.ru.nl>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: Coq Club <coq-club AT inria.fr>, Venanzio Capretta <vxc AT cs.nott.ac.uk>
Subject: Re: [Coq-Club] Tarski style universes in Coq
Date: Thu, 30 Aug 2012 09:20:49 +0200

Ideally something along the lines of:
http://www2.math.uu.se/~palmgren/universe.pdf

Unfortunately, Coq lacks support for induction-recursion.

Best,

Bas

On Wed, Aug 29, 2012 at 10:14 PM, Adam Chlipala
<adamc AT csail.mit.edu>
wrote:
> On 08/29/2012 04:05 PM, Bas Spitters wrote:
>>
>> Is there any work trying to mimick Tarski style universes in Coq?
>> I.e. defining universes using explicit codes.
>>
>
>
> Do you just mean defining a type of syntax for types, or do you have a
> particular class of supported types in mind?

[Coq-Club] Tarski style universes in Coq, Bas Spitters, 08/29/2012
- Re: [Coq-Club] Tarski style universes in Coq, Adam Chlipala, 08/29/2012
  - Re: [Coq-Club] Tarski style universes in Coq, Bas Spitters, 08/30/2012