Type Hierarchy in Agda

Question

I am trying to figure out how type hierarchies work in Agda.

Assuming I define a set type X:

X : Set 

and then proceed to constructing an inductive type

data Y : X -> Set where

What is the type of X -> Set? Is it Set or Type?

Thank you!

Answer 1

Well, why not ask Agda itself? I'm going to use excellent Agda mode for Emacs. We start with:

module Hierarchy where

postulate
  X : Set

data Y : X → Set where
  -- empty

We have to load the file using C-c C-l; this typechecks the file, turns ?s into holes, does syntax highlighting and so on.

Now, there is a command "Infer (deduce) type" available via C-c C-d, so let's use that:

> C-c C-d
Expression:
> Y
X → Set

Right, that makes sense. We defined Y : X → Set, so it should come as no surprise. Let's ask again:

> C-c C-d
Expression:
> X → Set
Set₁

So, there you have it: Y : X → Set : Set₁.

---

While the first part answers the question and shows you how to check this stuff yourself, doing that everytime would be dull, at least. Here's how it works:

To avoid paradoxes, we require

Set i : Set (i + 1)

which gives you the (infinite) hierarchy of Sets. If you had Set : Set (which Agda allows via the --type-in-type flag), you could derive contradiction such as this one.

This also gives us a simple rule for functions:

A : Set i
B : A → Set j

(a : A) → B a : Set (max i j)

Applying this to your example:

X   : Set
Set : Set₁

X → Set : Set (max 0 1)
X → Set : Set₁