"Realizing" Globular Sets in Homotopy Type Theory

Question

[Apologies in advance if I don't have the right terminology down for some things -- I'm a bit of a novice, hopefully not at the stage where I know enough to be dangerous, but not enough to be useful.]

I've seen the page on nLab about attempts to define semi-simplicial types in Homotopy Type Theory. From a trail of references, I saw that there's a reasonable co-inductive definition of a globular type.

Now, I can see a sort of parallel between finite globular sets and HITs which are generated only by 0-ary constructors, where every n-path constructor only depends on previously-defined (n-1)-paths, with no function applications allowed. (Which rules out composition of paths, in particular.) Is there a way to take a globular set and interpret it as if it presented such a HIT to yield a type? I'm looking for a function $Realizer : Glob \rightarrow Type$ such that the type it returns on a given globular set is equivalent to the result you'd get from transcribing everything to a new HIT where the point constructors are points of the globular sets, the 1-path constructors correspond to 1-globes of the globular set, the 2-path constructors correspond to 2-globes of the globular set, etc.

I'm not really sure if this is possible in the exact terms that I stated, so feel free to weaken/adjust things, or explain why it's hard or impossible. I'm also open to reference suggestions if this kind of thing has already been done, or if there are people out there pursuing something similar.

Big Edit: Mike Shulman pointed out that what I was originally asking for was nonsense, so I fixed up the middle section to be closer to what I'm looking for at a conceptual level.

Answer 1

Suppose we define finite-dimensional globular types recursively rather than coinductively:

gset (n : nat) : type
gset 0 = type
gset (n+1) = Sigma(G0 : type) (G0 -> G0 -> gset n).

Then we can define recursively a HIT that realizes any such:

realiz (n : nat) (G : gset n) : type
realiz 0 A = A
realiz (n+1) (G0 , Gn) = quotient G0 (\x y -> realiz n (Gn x y))

where quotient is the HIT "quotient" of a type-valued relation:

data quotient (A : type) (R : A -> A -> type) : type :=
| q : A -> quotient
| r : (a b : A) (r : R a b) -> (q a = q b)