List Set 应该是一种排序，但它不是

Question

我刚开始使用 Agda 来进行一些概念验证。

在这种情况下，我想要一个结构与下面定义的 Relation 相似的数据类型。

（为简单起见，省略了数据类型A的元素和函数relation-1的定义）。

当Relation这样定义时：

open import Data.Product using (_×_)
open import Data.List using (List; _∷_; [])
open import Data.Unit using (⊤)

data A : Set where

relation-1 : A → List A
relation-1 = {!!} 

map-1 : ∀{A : Set} → (A → Set) → List A → List Set
map-1 _ [] = []
map-1 p (a ∷ as) = p a ∷ (map-1 p as) 

map-2 : ∀{A : Set} → (A → Set) → List A → Set
map-2 p [] = ⊤
map-2 p (a ∷ as) = p a × (map-2 p as)

data Relation : A → Set where 
  refl : (a : A) → Relation a
  expand : (a : A) → map-1 Relation (relation-1 a) → Relation a

错误信息是：

List Set should be a sort, but it isn't
when checking that the inferred type of an application
  List Set
matches the expected type
  _43

但是，将 map-1 替换为 map-2 后

data Relation : A → Set where 
  refl : (a : A) → Relation a
  expand : (a : A) → map-2 Relation (relation-1 a) → Relation a

不会有类型错误。

我的问题是为什么在 Relation 中使用 map-1 时 List Set 不是有效类型？

它在 map-1 的定义和其他情况下工作良好，例如在异构列表中：

data HList : (List Set) → Set where
  [] : HList []
  _∷_ : {A : Set}{xs : List Set} → A → HList xs → HList (A ∷ xs)

Answer 1

我要的就是这里的All： https://plfa.github.io/Lists/#21511

List Set 应该是一种排序，但它不是

List Set should be a sort, but it isn't

agda