Tipo de jerarquía en Agda
Estoy tratando de averiguar cómo funcionan las jerarquías de tipos en Agda.
Suponiendo que defino un conjunto de tipo X:
X : Set
y luego proceder a construir un tipo inductivo
data Y : X -> Set where
Cual es el tipo deX -> Set
? ¿Es conjunto o tipo?
¡Gracias!