[Agda] Universe level checking

[Martin Escardo]

I am generalizing some old code by replacing `Set` with `Set ?` and
using ctrl-C-S to fill such holes when possible.

Am I right to think there is a problem with the following?

```
_∼_ : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
→ (X → Y) → (X → Y) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x

retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
→ (X → Y) → (Y → X) → Set ℓ'
retraction-section r s = r ∘ s ∼ id
```

I would have thought that the type of `retraction-section r s` should be
`Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.

It shouldn't be possible to construct something in a small universe
using ingredients from a large universe without the risk of paradox (but
I haven't paused to try to exploit this to get a contradiction).

Martin

[Andreas Abel]

Hi Martin,

completing your snipped with standard library imports, in particular

open import Function

for id and comp, I get the following error:

Set .ℓ' != Set (.ℓ ⊔ .ℓ')
when checking that the expression id has type .Y → .X

Is that the error you expected?

The answer is uniform for all Agda versions > 2.5, I did not try 2.4.

However, I can actually not get your code to type check at all. The
correct type for retraction-section is:

retraction-section : {ℓ : Level} {X Y : Set ℓ}
→ (r : X → Y) → (s : Y → X) → Set ℓ
retraction-section r s = (r ∘ s) ∼ id

with just a single level.

Best,
Andreas

Post by Martin Escardo
I am generalizing some old code by replacing `Set` with `Set ?` and
using ctrl-C-S to fill such holes when possible.
Am I right to think there is a problem with the following?
```
_∼_ : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
    → (X → Y) → (X → Y) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x
retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
                   → (X → Y) → (Y → X) → Set ℓ'
retraction-section r s = r ∘ s ∼ id
```
I would have thought that the type of `retraction-section r s` should be
`Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.
It shouldn't be possible to construct something in a small universe
using ingredients from a large universe without the risk of paradox (but
I haven't paused to try to exploit this to get a contradiction).
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Martín Hötzel Escardó]

Hi Andreas,

Thanks for the discussion.

My code compiles with 2.6.0-5135fd5 (in this machine now at home) and
with 2.6.0-3b39f0f (in my office machine when I posted the message).

I don't use the standard library, and all my files in this development
have --without-K --exact-split --safe.

Post by Andreas Abel
completing your snipped with standard library imports, in particular
open import Function
Set .ℓ' != Set (.ℓ ⊔ .ℓ')
when checking that the expression id has type .Y → .X

Perhaps you have a different definition of composition there (I don't
know). Mine is

_∘_ : {ℓ ℓ' ℓ'' : Level} {X : Set ℓ} {Y : Set ℓ'} {Z : Y → Set ℓ''}
→ ((y : Y) → Z y) → (f : X → Y) → (x : X) → Z(f x)
g ∘ f = λ x → g(f x)

Post by Andreas Abel
Is that the error you expected?

I don't get this error! I didn't expect any particular error.

Post by Andreas Abel
The answer is uniform for all Agda versions > 2.5, I did not try 2.4.

I think that, then, this must depend on the standard library. I am not
using it, as I said.

Post by Andreas Abel
However, I can actually not get your code to type check at all. The
retraction-section : {ℓ : Level} {X Y : Set ℓ}
→ (r : X → Y) → (s : Y → X) → Set ℓ
retraction-section r s = (r ∘ s) ∼ id
with just a single level.

I think it is perfectly fine for a large type to be a retract of a
small type. The question was rather whether "being a retract of a
large type" should be a small or large (Curry-Howard) proposition.

I may include a link to the source code and its compiled html version
if you wish, for inspection.

But I would like to clarify that my question was not so much an
Agda-specific one, but more of a philosophical one, thinking about
what the right rendering of universes in a dependendent type theory `a
la Martin-Loef is.

Best,
Martin

Post by Andreas Abel
Best,
Andreas

Post by Martin Escardo
I am generalizing some old code by replacing `Set` with `Set ?` and
using ctrl-C-S to fill such holes when possible.
Am I right to think there is a problem with the following?
```
_∼_ : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
→ (X → Y) → (X → Y) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x
retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
→ (X → Y) → (Y → X) → Set ℓ'
retraction-section r s = r ∘ s ∼ id
```
I would have thought that the type of `retraction-section r s` should
be `Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.
It shouldn't be possible to construct something in a small universe
using ingredients from a large universe without the risk of paradox
(but I haven't paused to try to exploit this to get a contradiction).
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Martín Hötzel Escardó]

Post by Martín Hötzel Escardó

Post by Andreas Abel
completing your snipped with standard library imports, in particular
   open import Function
   Set .ℓ' != Set (.ℓ ⊔ .ℓ')
   when checking that the expression id has type .Y → .X

So continuing the discussion from my previous message, I have created a
version exhibiting what I said (it would be nice to see which Agda
versions can compile it):

http://www.cs.bham.ac.uk/~mhe/agda-discussion/all.zip

The file in question (in its html rendering) is

http://www.cs.bham.ac.uk/~mhe/agda-discussion/Equivalence.html

where `retraction-section` is the second definition of the file.

Martin

Post by Martín Hötzel Escardó
Perhaps you have a different definition of composition there (I don't
know). Mine is
_∘_ : {ℓ ℓ' ℓ'' : Level} {X : Set ℓ} {Y : Set ℓ'} {Z : Y → Set ℓ''}
    → ((y : Y) → Z y) → (f : X → Y) → (x : X) → Z(f x)
g ∘ f = λ x → g(f x)

Post by Andreas Abel
Is that the error you expected?

I don't get this error! I didn't expect any particular error.

Post by Andreas Abel
The answer is uniform for all Agda versions > 2.5, I did not try 2.4.

I think that, then, this must depend on the standard library. I am not
using it, as I said.

Post by Andreas Abel
However, I can actually not get your code to type check at all.  The
   retraction-section : {ℓ  : Level} {X Y : Set ℓ}
                    → (r : X → Y) → (s : Y → X) → Set ℓ
   retraction-section r s = (r ∘ s) ∼  id
with just a single level.

I think it is perfectly fine for a large type to be a retract of a
small type. The question was rather whether "being a retract of a
large type" should be a small or large (Curry-Howard) proposition.
I may include a link to the source code and its compiled html version
if you wish, for inspection.
But I would like to clarify that my question was not so much an
Agda-specific one, but more of a philosophical one, thinking about
what the right rendering of universes in a dependendent type theory `a
la Martin-Loef is.
Best,
Martin

Post by Andreas Abel
Best,
Andreas

Post by Martin Escardo
I am generalizing some old code by replacing `Set` with `Set ?` and
using ctrl-C-S to fill such holes when possible.
Am I right to think there is a problem with the following?
```
_∼_ : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
     → (X → Y) → (X → Y) → Set (ℓ ⊔ ℓ')
f ∼ g = ∀ x → f x ≡ g x
retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
                    → (X → Y) → (Y → X) → Set ℓ'
retraction-section r s = r ∘ s ∼ id
```
I would have thought that the type of `retraction-section r s` should
be `Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.
It shouldn't be possible to construct something in a small universe
using ingredients from a large universe without the risk of paradox
(but I haven't paused to try to exploit this to get a contradiction).
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Stefan Monnier]

Post by Martin Escardo
retraction-section : {ℓ ℓ' : Level} {X : Set ℓ} {Y : Set ℓ'}
→ (X → Y) → (Y → X) → Set ℓ'
retraction-section r s = r ∘ s ∼ id

[...]

Post by Martin Escardo
I would have thought that the type of `retraction-section r s` should be
`Set (ℓ ⊔ ℓ')` rather than ` Set ℓ'`.

`r ∘ s` has type `Y -> Y`, where `Y : Set ℓ'`, so `Y -> Y : Set ℓ'`.
I don't see any reason for `ℓ` to appear in there at all.

It's perfectly OK for a function to return a value in a smaller universe
than some of its arguments. It's the *type* of that function which will
belong to a larger universe. E.g.

(X → Y) : Set (ℓ ⊔ ℓ')

and

(X → Y) → (Y → X) → Set ℓ' : Set (ℓ ⊔ (succ ℓ'))


-- Stefan

[Manny Romero]

_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

[Andreas Abel]

Manny,

you need to upgrade to a newer version of Agda. The latest release is
2.5.3.

7,12 : Parse error
constructor<ERROR>

This is because Agda 2.4 does not know about the "instance" keyword.

Alternatively, you could try to get an old version of Ulf's Prelude, the
one he used for the OPLSS. I have no clue if this is possible, though.

Best,
Andreas

I'm trying to follow the OPLSS 2014 Agda tutorial. As seen in the first
two minutes here (

), this
requires loading some files from agda-summer-school-OPLSS and
agda-prelude on this ( https://github.com/UlfNorell/agda-summer-school )
website.
Despite not knowing anything about computers, I think I've somehow
managed to both download these files and tell emacs where to look for
them successfully. The problem is that I now get error messages for
Prelude files when I try to load Day1.agda. For instance, when I do so,
the main screen shows "module Prelude.Unit where" followed by the rest
of Unit.agda from the Prelude subdirectory
-----------------------
module Prelude.Unit where
open import Agda.Builtin.Unit public
record ⊤′ {a} : Set a where
  instance constructor tt
-- To keep changes from compat-2.4.0 to a minimum.
Unit = ⊤
pattern unit = tt
-------------------------
and the screen below reads something like
-------------------------
7,12 :  Parse error
constructor<ERROR>
tt
--------------------------
When I comment out the text of this file and save, an error message for
another Prelude file pops up.
What might I be doing wrong? Surely there isn't really something wrong
with all these files? Why might this be happening to me?
I have Linux Mint 18, Agda 2.4.2.5, Emacs 24.5.1. And again, I am
completely computer illiterate and it's a minor miracle I managed to get
this far!
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Manny Romero]

_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

[Andrés Sicard-Ramírez]

I am now attempting to use cabal to install the newest Agda. It keeps
failing because of different programs I have not installed yet, so that's
what I'm doing now. I am stuck at this point on one in particular, cpphs.
What happened is I initially installed one version, 1.19.3, using "sudo apt
install", but this was apparently not as new as the Agda 2.5 requires.
I was
able to use cabal to install the latest, cabal-1.20.8, but apparently this
does not affect what is found under usr/bin/cpphs. Nor can I use the "sudo
apt install cabal-1.20.8" at this point; it reports that it cannot find it.
What is going on here?

It seems you installed two versions of cpphs:

cpphs 1.19.3 in usr/bin/cpphs (vía sudo apt install) and

cpphs 1.20.8 in ~/.cabal/bin/cpphs (via cabal install)

but you didn't add the directory ~/.cabal/bin to your path.

Note: The directory ~/.cabal/bin should be the first one in your path.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.

[Manny Romero]

_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

[Andrés Sicard-Ramírez]

It is weird that you have this problem after fixing the cpphs problem.

If you installed Agda 2.4.2.5 from your distribution, please remove it.

Which is the output of

$ type agda

?

Using this advice I was able to install the new version (or so it would
----------
Configuring Agda-2.5.3...
Building Agda-2.5.3...
Installed Agda-2.5.3
----------
...but when I enter "Agda --version"
I still get 2.4.2.5
and the original tutorial problems, resulting from the earlier version,
persist as before.
(Also: I added this
----------
PATH=~/.cabal/bin:$PATH
export PATH
-----------
to the end of my ~/.profile document, as suggested on the Internet. But it
doesn't change my path when I call up a fresh session. What did I do wrong?
--Note: I don't think this problem is related to the first, because I was
checking the Agda version from within the same session with the altered path
that enabled me to finally install the 2.5 Agda in the first place.)
Sent: Saturday, December 02, 2017 at 6:01 PM
Subject: Re: [Agda] Trying to load modules from Norell OPLSS tutorial

I am now attempting to use cabal to install the newest Agda. It keeps
failing because of different programs I have not installed yet, so that's
what I'm doing now. I am stuck at this point on one in particular, cpphs.
What happened is I initially installed one version, 1.19.3, using "sudo apt
install", but this was apparently not as new as the Agda 2.5 requires.
I was
able to use cabal to install the latest, cabal-1.20.8, but apparently this
does not affect what is found under usr/bin/cpphs. Nor can I use the "sudo
apt install cabal-1.20.8" at this point; it reports that it cannot find it.
What is going on here?

cpphs 1.19.3 in usr/bin/cpphs (vía sudo apt install) and
cpphs 1.20.8 in ~/.cabal/bin/cpphs (via cabal install)
but you didn't add the directory ~/.cabal/bin to your path.
Note: The directory ~/.cabal/bin should be the first one in your path.
--
Andrés
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.

[Manny Romero]

_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

[Andrés Sicard-Ramírez]

I will make you some questions off the mailing list.

I used "sudo apt remove agda". It reported success, and when I attempt to
repeat the command it reports that it is not installed so cannot be removed.
However, "agda --version" still results in "Agda version 2.4.2.5". And "type
agda" results in "agda is hashed (/usr/bin/agda)".
Note that success was reported from the previous attempt at installing 2.5.
It did take a very long time to install, but it printed the success message
copied below verbatim.
Sent: Saturday, December 02, 2017 at 11:12 PM
Subject: Re: [Agda] Trying to load modules from Norell OPLSS tutorial
It is weird that you have this problem after fixing the cpphs problem.
If you installed Agda 2.4.2.5 from your distribution, please remove it.
Which is the output of
$ type agda
?

Using this advice I was able to install the new version (or so it would
----------
Configuring Agda-2.5.3...
Building Agda-2.5.3...
Installed Agda-2.5.3
----------
...but when I enter "Agda --version"
I still get 2.4.2.5
and the original tutorial problems, resulting from the earlier version,
persist as before.
(Also: I added this
----------
PATH=~/.cabal/bin:$PATH
export PATH
-----------
to the end of my ~/.profile document, as suggested on the Internet. But it
doesn't change my path when I call up a fresh session. What did I do wrong?
--Note: I don't think this problem is related to the first, because I was
checking the Agda version from within the same session with the altered path
that enabled me to finally install the 2.5 Agda in the first place.)
Sent: Saturday, December 02, 2017 at 6:01 PM
Subject: Re: [Agda] Trying to load modules from Norell OPLSS tutorial

I am now attempting to use cabal to install the newest Agda. It keeps
failing because of different programs I have not installed yet, so that's
what I'm doing now. I am stuck at this point on one in particular, cpphs.
What happened is I initially installed one version, 1.19.3, using "sudo apt
install", but this was apparently not as new as the Agda 2.5 requires.
I was
able to use cabal to install the latest, cabal-1.20.8, but apparently this
does not affect what is found under usr/bin/cpphs. Nor can I use the "sudo
apt install cabal-1.20.8" at this point; it reports that it cannot find it.
What is going on here?

cpphs 1.19.3 in usr/bin/cpphs (vía sudo apt install) and
cpphs 1.20.8 in ~/.cabal/bin/cpphs (via cabal install)
but you didn't add the directory ~/.cabal/bin to your path.
Note: The directory ~/.cabal/bin should be the first one in your path.
--
Andrés
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial
reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial
reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.
La información contenida en este correo electrónico está dirigida únicamente
a su destinatario y puede contener información confidencial, material
privilegiado o información protegida por derecho de autor. Está prohibida
cualquier copia, utilización, indebida retención, modificación, difusión,
distribución o reproducción total o parcial. Si usted recibe este mensaje
por error, por favor contacte al remitente y elimínelo. La información aquí
contenida es responsabilidad exclusiva de su remitente por lo tanto la
Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The
information contained in this email is addressed to its recipient only and
may contain confidential information, privileged material or information
protected by copyright. Its prohibited any copy, use, improper retention,
modification, dissemination, distribution or total or partial reproduction.
If you receive this message by error, please contact the sender and delete
it. The information contained herein is the sole responsibility of the
sender therefore Universidad EAFIT is not responsible for what the message
contains.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.