Agda type error

Question

I am new to Agda, and I am attempting to define a constant prod of type: Z → (Z → ((Z → Set) → Set))

Now, I have written the following Agda code:

data Prod (X : Set) : ℕ → X where 
prod : ℕ → (ℕ → ((ℕ → X) → X))

When I type-check it, agda produces this error message:

X != Set (_33 X_) of type Set 
when checking the definition of Prod 

Any help is highly appreciated

Answer 1

Your data type definition has two problems. Firstly, all data types are in Set (of some level), you can't just go around and declare data types as being elements of some other type.

data T : ℕ where

This definition tries to postulate that there's another element of the natural numbers, namely T. That doesn't make much sense. The only possible "type" to which you can add more elements is Set - the type of all (small) types. (I'm glossing over the fact that there's an infinite hierarchy of Sets, you shouldn't need to deal with that now).

So this is okay:

data T : Set where

---

The second problem with your definition is that the type of the prod constructor doesn't reflect that it really constructs something of type Prod. The point of constructors is that they can be an element of the type you are defining.

Let's take a look at the definition of natural numbers:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

When we write zero : ℕ, we are saying that zero is a natural number. What if we had this instead:

data ℕ : Set where
  zero : String
  suc  : ℕ → ℕ

We are defining natural numbers and we define that zero is a String? So, since we are defining constructors, the type we give to it must mention the type we are defining in the last position. (This mention can also be indirect).

Op₂ : Set → Set
Op₂ A = A → A → A

data Tree (A : Set) : Set where
  nil  :          Tree A
  node : A → Op₂ (Tree A)

---

You can add parameters to the left of the colon, you cannot change those in the constructors. So for example, this is invalid:

data T (A : Set) : Set where
  t : T ℕ

Notice that T alone is not enough - it's not a type, but something like function from types to types (i.e. Set → Set). This one is okay:

data T (A : Set) : Set where
  t : T A

To the right of the colon are indices. These are something like parameters, except that you can choose the value in the constructors. For example, if we have a data type indexed by natural number, such as:

data T : ℕ → Set where

You can have constructors like:

data T : ℕ → Set where
  t₀ : T zero
  t₁ : T (suc zero)

Much like above, T alone is not a type. In this case it's a function ℕ → Set.

---

Anyways, back to your code. If you meant Prod to contain one function of type ℕ → (ℕ → ((ℕ → X) → X)), then it should be:

data Prod (X : Set) : ℕ → Set where
  prod : (ℕ → (ℕ → ((ℕ → X) → X))) → Prod X zero

However, I have no idea what was your intention with the index.