HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to d

HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions. The resulting constructions can be interpreted as talking about properties of spaces. The rules themselves are very stripped-down and abstract when viewed in a homotopical light, like "every path can be retracted to an endpoint" or "the interval has two points and a path between them". Originally the basic rule for reasoning about paths ("path induction") was intended to allow construction of equality proofs between elements of types. Later people discovered that equalities can be interpreted as paths in spaces (and equalities of equalities as homotopies and so on). Remarkably, the four typing rules of equality suffice to generate all homotopical reasoning in classic HoTT. However, they aren't enough to prove univalence as a theorem, or at least no one knows how to do it. If we switch to cubical type theory, we get considerably more structure which allows us to prove univalence. But cubical type theory is also "synthetic" and builds up notions of spaces from ground-up.