I'm trying to define n-globs, for each n. I'm trying to do this in terms of an indexed family of higher inductive types. I think I have a working definition but it is almost intractable and hard to work with. Here is what I have so far:
Define 0-glob via:
G0 : 0-glob
Define 1-glob via:
in$_1$ : 0-glob $\to$ 1-glob
G0$_2$ : 1-glob
G1 : in$_1$(G0) = G0$_2$
Assuming we have the n-glob and the n+1-glob, define (n+2)-glob via:
in$_{n+2}$ : (n+1)-glob $\to$ (n+2)-glob
G(n+1)$_2$ : in$_{n+2}$(in$_{n+1}$(Gn)) = in$_{n+2}$(Gn$_2$)
G(n+2) : in$_{n+2}$(G(n+1)) = G(n+1)$_2$
The idea behind this is that an n+1-glob contains "a copy" of the n-glob, so we should have in$_{n+1}$:n-glob $\to$ n+1-glob. But, the n+1 glob contains another n-morphism parallel to the copied n-morphism. This is why I have the G(n+1)$_2$; it is supposed to be that parallel n-morphism. Finally, the n+1-glob has a n+1-morphism filling the frame of the two parallel n-morphisms. I think everything is well typed in the definition.
My problem is that this definition is, well, gross. The elimination principle for even just 2-glob will not be nice to work with. The main difficulty is the "in" constructor at each level. But, I do not know how I could remove this constructor. So, my question is how are n-globs defined as HITs? I could not find anything else where online.
I doubt you'll find anyone defining n-globes as HITs because they are not homotopically very interesting: they are all contractible!
That said, your definition looks like it might be sensible. But I think an easier definition would be to induct at the bottom: the $(n+1)$-globe has two points $s,t$ and a map from the $n$-globe into $s=t$.