Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] What is a successor universe?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] What is a successor universe?


Chronological Thread 
  • From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] What is a successor universe?
  • Date: Thu, 17 Jan 2019 15:36:38 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f173.google.com
  • Ironport-phdr: 9a23:ocOTyhSLE+zhqYlzGp9jlntZLtpsv+yvbD5Q0YIujvd0So/mwa69ZxSN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMPpCr4nhp1sOsAG+DhSwCeLu1DBImGH50rA90+88DA7JwhErEs4LsHTTttX1NaISWv2ywabS1zXDc/NW2Srn6ITSaB8uu+qBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWuD7+d4S+6jl2oqpxtyrzWv3Msgl4jEi4APxlzZ9yh0zoA4LsCiRkFhe96rCp5QujmaN4RoRsMiRHlluCMgxb0HvZ63ZS8KyJU6yxLGZfyLboqF7xz5WOaeJjd4g31leLahiBqo7Uegzej8WtG10FZMsCVFjsHBum4R2xHX8MSKSftw8l281TuO1Q3f8PxILEI6mKbDLp4u2L8wlp4dsUTZGS/2nV37g7WMdkU4+uio9v7nbq/8qZCGLIJ0hQT+Pb4vmsy7G+g3Lg8OX22D9eSmyLLj5VH5QKlNjvAujqbZt4naKd0Hqa69Hg9ayZ0u6w2/DjejyNQXh2MLLFNDeBKdjojmIUvCIP7iDaT3v1P5mzBygvvCI7fJA5PXL3GFnq2yU6x67ht10hYz0MoXzoBZFLwNJ7r/VwfYsdvCDxpxZwWu3+b6EpN036sRXGuOBumSN6aE4gzA3f4mP+TZPNxdgz36MfVwv6e/3098okcUeOyS5bVSbXm5Gvp8JEDAOCjjh94AFSEBuQ9sFbW22m3HaiZaYjOJZ4x5/isyUdv0AoLKR4Tri7uEjn/iQ89mI1teA1XJKk/GMoWJX/BWNnCXK85l1zsFDP2vEtB6kx6pswD+xvxsKe+GoiA=

Yes, if algebraic universes are not allowed in definitions, it makes sense that these upper bounds need to be explicitly declared. Why isn't it possible for definitions to include algebraic universes?

Em qui, 17 de jan de 2019 às 12:04, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> escreveu:

 > If I omit the annotation, Coq complains that I haven't declared the
 > universe where the definition should live:

This is because it needs to live in some upper bound universe, as i+1
isn't allowed. ie


Polymorphic Definition pack2@{i j|i < j} (T : Type@{i}) (x : T) :
pack@{j} :=
   Pack pack@{i} (Pack@{i} T x).


Gaëtan Gilbert

On 17/01/2019 15:18, Arthur Azevedo de Amorim wrote:
> Coq accepts the following snippet, which declares a universe-polymorphic
> type that lives in a successor universe:
>
> Polymorphic Inductive pack@{i} : Type@{i+1} :=
>    Pack { sort : Type@{i}; elt : sort }.
>
> However, if I try to take the successor of a universe level elsewhere, I
> get a parse error:
>
> Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) : pack@{i+1} :=
>    Pack pack@{i} (Pack@{i} T x).
>
> (* Toplevel input, characters 65-66: *)
> (* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :
> pack@{i+1} :=   Pack pack@{i} (Pack@{i} T x). *)
> (* >                                                                  ^ *)
> (* Error: Syntax error: [constr:universe_level] or '}' expected (in
> [instance]). *)
>
> If I omit the annotation, Coq complains that I haven't declared the
> universe where the definition should live:
>
> Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=
>    Pack pack@{i} (Pack@{i} T x).
> (* Toplevel input, characters 61-65: *)
> (* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=   Pack
> pack@{i} (Pack@{i} T x). *)
> (* >                                                              ^^^^ *)
> (* Error: Universe {Top.72} is unbound. *)
>
> Is there any way of convincing Coq that pack2's codomain is pack@{i+1}?
>
> Thanks!
>
> Best,
> Arthur



Archive powered by MHonArc 2.6.18.

Top of Page