Using induction to define Indexed family of HITs in agda

Question

I am looking to define a family of HITs parametrized by $\mathbb{N}$. I want $(-)$-glob : $\mathbb{N} \to Type$, so that $n$-glob is the n-dimensional glob. I know how to construct the n-$glob$ by induction on $n$. The problem I am running into is that I do not know how to use induction on $\mathbb{N}$ in the middle of the definition of a HIT. For example, I have the code

data _-glob (n : ℕ) : Type where

and I want to case on $n$ so that I may specify what $n:\equiv 0$ is and what $n:\equiv suc (n)$ is, given what $n$ is. But, I cannot simply write

data _-glob (n : ℕ) : Type where
 H : ?

and then case on $n$. Does anyone know how to use induction in the middle of such a definition?

EDIT: Here is my (quite literal) "black board" inductive definition of _-glob. Its pretty messy and I'm sure there are more elgant ways to define it but this is what I'm trying to turn into agda code:

0-glob where

 G0 : 0-glob


1-glob where

 in : 0-glob -> 1-glob

 G0_2 : 1-glob

 G1 : in(G0) = G0_2


(n+2)-glob where

 in : (n+1)-glob -> (n+2)-glob

 G(n+1)_2 : in(in(Gn)) = in(Gn_2)

 G(n+2) : in(G(n+1)) = G(n+1)_2

Now, I'm pretty sure this give me what I want. 1-glob is equivalent to the interval. 2-glob contains a copy of 1-glob, via the constructor "in". But, 2-glob contains and additional path parallel to the preexisting one. And it contains a two path between these 1 paths. But, to actually define this as a HIT (in one go), i would need to case on n to specify the constructors.

Answer 1

Use

data _-glob : ℕ -> Type where

Now you can just do something like H : blabla -> zero -glob. Warning: This is called an indexed inductive family, and cubical Agda still has some unimplemented functionalities about this feature yet. You might want to look at the standard library (not the cubical library) on the Fin type to see an example.

Another way to do it is as a recursive type. You first define zero-glob separately. Then you define suc-glob (n-glob : Type) : Type. Now take

_-glob : (n : ℕ) -> Type
zero -glob = zero-glob
(suc n) -glob = suc-glob (n -glob)