coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tarski style universes in Coq

From: Bas Spitters <spitters AT cs.ru.nl>
To: Coq Club <coq-club AT inria.fr>
Cc: Venanzio Capretta <vxc AT cs.nott.ac.uk>
Subject: [Coq-Club] Tarski style universes in Coq
Date: Wed, 29 Aug 2012 22:05:31 +0200

Is there any work trying to mimick Tarski style universes in Coq?
I.e. defining universes using explicit codes.

Venanzio Capretta shows how to mimick induction-recursion in Coq, but
explicitly excludes its application to defining universes.
http://www.cs.ru.nl/~venanzio/publications/induction_recursion.pdf

Thanks,

Bas

[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