Dans le GADT d'Agda, est «paramétré» et «indexé» différents sémantiquement?

Question

Je sais qu'ils ont une différence dans la portée:

data a (n : Set) : Set where
    introA : a n

data b : Set -> Set where
    introB : {n : Set} -> b n

C'est ne pas ce qui me soucie. Sont-ils différents sémantiquement?