Not supporting HIT in dependent type? about cubical

[Saizan]

The problem is that Ω n .. does not reduce, because Ω is defined by pattern matching on the natural number.

That's what the error message is trying to say

The target of a constructor must be the datatype applied to its
parameters, Ω n (Sphere n , base n) .fst isn't
when checking the constructor cell in the declaration of Sphere

"The target of a constructor must be the datatype applied to its parameters" means that the result type of a constructor should reduce to "Sphere .."

The other examples work because e.g. (Ω 2 (S² , base)) .fst normalizes to (λ _ → base) ≡ (λ _ → base) which is a path type in S².

[mortberg]

This HIT is not supported by what we did in

https://arxiv.org/abs/1802.01170

or by the schema of

http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf

It is in some sense clear that it works semantically as the types are equivalent to the spheres for a fixed n, but it is not clear how to get it to work type theoretically. A concrete issue is how to even write down the eliminator in general. Given n : ℕ what do we do in the cell case? We will need to give an equation of the form:

f (cell i_1 ... i_n) = 

but you cannot write "..." in type theory.