Agda疑问：数据定义中编译器为何要求Set₁而非Set？

问题重现 #

尝试在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₁后，代码可以正常编译：

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₁

错误原因 #

问题核心在于索引与参数的区别以及Agda的宇宙层级规则：

• 最初的定义中，A和B是作为datatype的索引（写在:之后的部分），而非参数（写在data名称后的括号内）。
• 索引的类型是Set（即Set₀），而Set本身属于Set₁宇宙。Agda要求datatype的宇宙层级必须大于等于其索引类型的宇宙层级——你定义的_×_属于Set（Set₀），但索引的类型属于Set₁，违反了Set₁ ≤ Set₀的层级规则，因此报错。
• 改成Set₁后，datatype的宇宙层级是Set₁，满足Set₀ ≤ Set₁，所以编译通过，但此时A × B属于Set₁而非预期的Set，不符合常规集合积的类型。

正确的定义方式 #

常规的集合积类型应该将A和B作为datatype的参数，而非索引，这样既符合宇宙层级规则，又能让A × B属于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

-- 参数化的集合积定义，A、B是datatype参数
data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

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

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

这里A和B是datatype的参数，每个参数组合对应独立的积类型，构造函数的参数类型A、B都属于Set，与datatype的宇宙层级一致，完全符合Agda的规则。

关于--large-indices选项 #

错误信息中提到的--large-indices是Agda的一个扩展选项，开启后允许索引类型的宇宙层级大于等于datatype的宇宙层级，这样你最初的定义可以编译。但这种写法会打破宇宙层级的累积性，可能导致逻辑不一致，因此不推荐在常规场景下使用。

内容的提问来源于stack exchange，提问作者Артём Мухамед-Каримов МПБ-802