Example "Type 1", which is neither a "Type" nor a resident of the "Type"

Question

What is an example of a Type 1 resident who is neither a Type nor a Type resident? I could not come up with anything while researching in the Idris REPL.

To be more precise, I am looking for a few x , except for Type , which gives the following:

 Idris> :tx x : Type 1 

Answer 1

I am not a specialist in type theory, but here is my understanding. The Idris textbook has a section 12.8 Cumulativeness . It says that there is an internal hierarchy of universes like:

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

And for any x : Type n it follows x : Type m for any m > n . There is also an example demonstrating how it prevents possible type inference loops.

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

See also nLab articles on universes in type theory and type types .

Perhaps this issue in the idris-dev repository can also be useful. Edwin Brady refers to the Design and Implementation document (see Section 3.2.2).

Answer 2

I am not an expert in Idris, but I expect that

 Type -> Type 

also located in Type 1 .

I would also expect

 Nat -> Type 

and if you are very lucky (not so sure about this)

 List Type 

to be so big.

The idea is that you can perform all font creation operations at each level. Each time you use types from one level as values, the types of these structures live one level up.