[Agda] This ain't right, is it?

[Dan Doel]

On Friday 30 October 2009 7:54:56 pm Benja Fallenstein wrote:
> The following type-checks with the darcs version of Agda (and
> --universe-polymorphism):
> 
> IsThatRight : {i : Level} → Set i
> IsThatRight {i} = (R : Set i) → R
> 
> Isn't that like set-in-set? Agda does object to this:

Technically, this wouldn't be Set : Set. It'd be impredicativity if we still 
have:

  Set i : Set (suc i)

but

  (R : T) -> E[R] : Set j where E[R] : Set j
    (instead of Set (max i j) with T : Set i)

However, impredicativity leads to similar problems as Set : Set in all but the 
lowest level (so you can have that rule for Prop or Set 0 ; Coq has the former 
and an option for the latter; this is as long as Prop : Set 0 isn't the case 
as well, in Coq, both have type analogous to Set 1).

My home-made type checker with universe polymorphism says

 (\(i : Level) -> (R : Type[i]) -> R) : (i : Level) -> Type[i + 1]

-- Dan