I was experimenting cubical Agda with {-# OPTIONS --cubical --rewriting #-}

I tried to define S^2, S^3 separately and found HIT worked fine.

However when I was trying to write down Sphere n for general natural number n it simply won't allow me to do so.

And the error message is "The target of a constructor must be the datatype applied to its parameters".

So how do I define a dependent HIT?

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)  -- Error!

222222222222