[Agda] Universe level checking

[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

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/