Agda：为什么编译器在数据定义中要求 Set_1，而不是 Set？

Question

尝试在 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

这会产生以下错误：

 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.

我不知道出了什么问题。两组的乘积必须是

Set

，而不是

Set₁

。但由于某种原因，以下编译得很好（我用

Set -> Set -> Set

替换了

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₁

Answer 1

问题出在语法上。以下方法成功了：

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