# “Realizing” Globular Sets in Homotopy Type Theory

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

• Even in classical homotopy theory, a space can't be recovered from its globular nerve the way it can from its simplicial nerve; globular sets just don't contain enough information (they don't tell you anything about path composition). – Mike Shulman Aug 29 '17 at 16:35
• Right, I can't think about e.g. a way to express a torus as a globular set, but circles and spheres would be fair game. I guess what I'm asking for is more subtle -- the types should be restricted to only those definable as HITs without reference to composition of paths, and where all of the constructors (point constructors and higher constructors) are 0-ary, and all constructors involving the nth identity type only involve named members of (n-1)th-identity types (no functions thereof). The "globular sets" here would actually be reflexive globular sets (due to the presence of refl). – user642291 Aug 29 '17 at 18:19
• I guess I should edit the middle section of the question, because I'm just realizing that it's complete nonsense [because e.g. for the circle, the derived globular set would be infinite] -- really, I'm just looking for something that takes a globular set mirroring the specification of a type via a HIT in the format described in my previous comment, and builds a type out of it which is equivalent to the one you'd get out of the spec as a HIT. – user642291 Aug 29 '17 at 18:30

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)