Example of a `Type 1` that is neither `Type` nor an inhabitant of `Type`

Question

What is an example of an inhabitant of Type 1 that is neither Type nor an inhabitant of Type? I wasn't able to come up with anything while exploring in the Idris REPL.

To be more precise, I'm looking for some x other than Type that yields the following:

Idris> :t x
x : Type 1

Answer 1

I'm not an Idris expert, but I'd expect that

Type -> Type

is also in Type 1.

I'd also expect

Nat -> Type

and if you're very lucky (not so sure about this one)

List Type

to be that large.

The idea is that you can do all type-building operations at every level. Each time you use types from one level as values, the types of those structures live one level up.

Answer 2

I'm not a type theory specialist, but here is my understanding. In the Idris tutorial there is a section 12.8 Cumulativity. It says that there is an internal hierarchy of type universes:

Type : Type 1 : Type 2 : Type 3 : ...

And for any x : Type n implies x : Type m for any m > n. There is also an example demonstrating how it prevents possible cycles in the type inference.

But I think that this hierarchy is only for internal use and there is no possibility to create a value of Type (n+1) which is not in Type n.

See also articles in nLab about universes in type theory and about type of types.

Maybe this issue in the idris-dev repository can be useful too. Edwin Brady refers there to the Design and Implementation paper (see section 3.2.2).