The Coq mailing list

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

On 18.04.11 5:41 PM, Randy Pollack wrote:
> Agda has some nearly-first-class treatment of universe levels.  I
> don't know what the theory behind it is.

We are working on it... ;-)  The theory should become clearer in the 
near future.

Cheers,
Andreas


> Matita (from Bologna) has some kind of explicit universe notation.
>
> Look at the very old paper  by Robert Harper and myself: "Type
> checking with universes" Theoretical Computer Science, 89:107-136,
> 1991 (file attached), where we give a detailed account of typical
> ambiguity and type polymorphism (not the same thing) in a slightly
> simpler system than the current CIC.
>
> Randy
> --
> On Mon, Apr 18, 2011 at 9:51 AM, Vladimir 
> Voevodsky<vladimir AT ias.edu>
>   wrote:
> > Dear Carlos,
> >
> > there is no need to introduce a new universe every time "Type" is mentioned. 
> > At the beginning of the file one declares the universe structure which one wants to 
> > work with by something like
> >
> > Variable UU0 UU1 : Univ.
> >
> > etc.
> >
> > (of course currently there is no identifier Univ and also Univ is not a type. 
> > May be one should use something other than : with Univ.)
> >
> >
> > Then  one can have a definition like that:
> >
> > Definition iscontr {U:Univ}(T:U) : U := ....
> >
> > which is polymorphic or like that
> >
> > Definition trrr (T:UU0):UU0 :=
> >
> > which assumes a fixed universe UU0.
> >
> >
> > Vladimir.
> >
> >
> >
> >
> > On Apr 16, 2011, at 10:26 AM, Carlos Simpson wrote:
> >
> > > Dear Vladimir,
> > >   It may be an interesting theoretical question to try to understand
> > > what happens if we try to make all definitions parametric over universes.
> > > Of course each time you make a new definition this introduces possibly many
> > > new universe indices. It could have something to do with quantum mechanics
> > > in that the ``universes'' which occur here might be related to the
> > > ``universes'' in the many-universe interpretation of quantum mechanics.
> > > ---Carlos Simpson
> > >
> > >
> > > Selon Vladimir 
> > > Voevodsky<vladimir AT ias.edu>:
> > >
> > > > Uhhh-uhh. I see. I got so used working with fixed universes that I forgot
> > > > about this behavior. Thanks! V.
> > > >
> > > > On Apr 15, 2011, at 7:24 PM, Tom Prince wrote:
> > > >
> > > > > On 2011-04-15, Vladimir Voevodsky wrote:
> > > > > > In the following example:
> > > > > >
> > > > > > File 1 (ex1.v) :
> > > > > >
> > > > > > Definition dneg (X:Type) := ((X ->  Empty_set) ->  Empty_set).
> > > > > >
> > > > > >
> > > > > > File 2 (ex2.v):
> > > > > >
> > > > > > Require Export ex1.
> > > > > > Variable X:Set.
> > > > > > Check (dneg X).
> > > > > > Check ((X ->  Empty_set)->  Empty_set).
> > > > > >
> > > > > >
> > > > > > Coq responds that (dneg X) is in Type while ((X ->  Empty_set)->  Empty_set)
> > > > is in Set. This does not look right.
> > > > > This is expected. Everything in Set is also in type, so
> > > > >
> > > > > Check ((X ->  Empty_set)->  Empty_set) : Type.
> > > > >
> > > > > Unfortunately, coq doesn't currently support looking through the
> > > > > definition of dneg to see that (dneg X) is convertible with a term of
> > > > > sort Set.
> > > > >
> > > > > There is limited support for doing this with paramaters of inductives,
> > > > > but nothing else.
> > > > >
> > > > > Tom

--
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/