Я пытаюсь выяснить, как иерархии типов работают в Agda.

Предполагая, что я определяю тип набора X:

X : Set 

а затем приступить к построению индуктивного типа

data Y : X -> Set where

Какой типX -> Set? Это набор или тип?

Спасибо!