[Agda] Universe level checking

[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.

On 29/11/17 19:30, andreas.abel at ifi.lmu.de wrote:
> 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

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)

> Is that the error you expected?

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

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

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

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

> 
> Best,
> Andreas
> 
> On 29.11.2017 16:50, Martin Escardo wrote:
>> 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
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 

-- 
http://www.cs.bham.ac.uk/~mhe