Search code examples
setagda

Agda: Why does the compiler demand Set_1, not Set in a data definition?

Tried to define a simple set product in Agda 2.6.4:

module Bool where
open import Function using (id ; const ; _∘_ ; _$_ )
open import Agda.Primitive

variable
  a : Level
  A B C : Set

data _×_ : Set -> Set -> Set where -- conjunction
   _,_ : A -> B -> A × B

Which yields the following error:

 C:\Users\...\Bool.agda:11,4-7
Set₁ is not less or equal than Set
when checking that the type Set of an argument to the constructor
_,_ fits in the sort Set of the datatype.
Note: this argument is forced by the indices of _,_, so this
definition would be allowed under --large-indices.

I have no idea what went wrong. The product of two sets must be a Set, not Set₁. But for some reason the following compiles just fine (I replaced Set -> Set -> Set with Set -> Set -> Set₁).

module Bool where
open import Function using (id ; const ; _∘_ ; _$_ )
open import Agda.Primitive

variable
  a : Level
  A B C : Set
  A₁ A₂ B₁ B₂ : Set a

data _×_ : Set -> Set -> Set₁ where -- conjunction
   _,_ : A -> B -> A × B

fst : A × B -> A
fst (x , x₁) = x

snd : A × B -> B
snd (x , x₁) = x₁
Solution

  • This is more than a syntactic difference. Your original definition had A and B as indices of the data type _x_ while your new definition had A and B as parameters.

    This makes a difference for the universe level of the data type, because in the first case the type A x B contains values of the form _,_ {A} {B} a b for A, B : Set, a : A and b : B. In other words, values of the type A x B contain the types A and B, which is why Agda insists that the type must live in a larger universe.

    When A and B are parameters, then the type A x B contains values of the form _,_ a b, i.e. the values do not "contain" the types A and B, which is why the type can live in the universe Set.