Not supporting HIT in dependent type?

[3abc]

In the following code I was trying to define Sphere n as a HIT depending on n. If I do this with S² or S³ it works fine. But it won't check Sphere n if I uncomment cell. In theory this should work, right?

PtType : Set₁
PtType = Σ Set (λ A → A)

Ω1 : PtType → PtType
Ω1 A = ((A .snd) ≡ (A .snd)) , refl

Ω : (n : ℕ) → PtType → PtType
Ω 0 A = A
Ω (suc n) A = Ω1 (Ω n A)

data S² : Set where
  base : S²
  surf : (Ω 2 (S² , base)) .fst

data S³ : Set where
  base : S³
  cell : (Ω 3 (S³ , base)) .fst

data Sphere : ℕ → Set where
  base : (n : ℕ) → Sphere n
  --cell : (n : ℕ) → (Ω n (Sphere n , base n)) .fst

[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.