[Agda] Universe level checking

[Martín Hötzel Escardó]

On 29/11/17 20:50, Martín Hötzel Escardó wrote:
> 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

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

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