列表集应该是一个排序，但它不是

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中使用List Set时，map-1不是有效的类型？

它在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