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

Question

I just start using Agda to work on some proof of concept.

In this case, I want a data type with similar structure as Relation defined below.

(for simplicity, the element of data type A and definition of function relation-1 are omitted).

When Relation is defined like this:

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 

The error message is :

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

However, after replacing map-1 with map-2

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

there will be no type error.

My question is why List Set is not a valid type when map-1 is used in Relation ?

It works well in the definition of map-1 and in other cases such as in the heterogeneous list:

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

Answer 1

What I want is just the All here : https://plfa.github.io/Lists/#21511