Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda An observation when defining List in agda with --without-K enabled:
The following parameterized inductive definition is accepted:
data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

but not the equivalent inductive family definition:
data List' : Set → Set where 
    []'  : {A : Set} → List' A
    _::'_ : {A : Set} → A → List' A → List' A

The error message is Set₁ is not less or equal than Set, so I have to change the type from List' : Set → Set to List' : Set → Set₁ in order for it to type-check. If I disable --without-K, then agda also correctly type-checks.
I tried to look up why this is the case, e.g., on the page https://agda.readthedocs.io/en/latest/language/without-k.html it says &quot;When --without-K is enabled, some indexed datatypes must be defined in a higher universe level. In particular, the types of all indices should fit in the sort of the datatype.&quot; But it doesn't say the reason for such difference between inductive family (indexed datatypes) definition and the parameterized inductive definition. I guess it has something to do with the homotopy model interpretation of the underlying type theory. However I want to know what sort of &quot;bad&quot; thing will happen if the inductive family lives in a smaller universe (syntax and semantics). And how would parameterized inductive definition avoids such issue?
Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a paradox will not work.
However, the above reasoning basically presumes K for the universe. Really all we can say is that knowing the type List A lets us know that the stored type is equal to A, but without K, we don't know that there are no non-trivial equalities between types. I'm not sure if there is an example of how this extra degree of freedom would allow a paradox to be written, but even if no example is known, it is safer to require the larger size than to assume that the small size is consistent.