## Simplicial sets, CW complexes

Simplicial sets can be described completely algebraically, by specifying a family of sets, and maps between them satisfying certain relations. This description can be directly derived from the nice abstract definition as presheaves over, or free cocompletion of, the simplex category.

The standard definition CW-complexes is more homotopy-theoretic in nature at first glance, but if you build one up inductively, you can usually describe in a completely syntactic way which cells you attach to which ones. And indeed, there is a big computational topology machinery behind them. Furthermore, higher inductive types try to give (amongst many other things) a syntactical theory to CW-complexes, and use them for homotopy type theory.

## Handle decompositions

I'm looking for something like this in the realm of handle decompositions. One often hears statements like "Handle decompositions are like CW-decompositions, but for manifolds", and in a lot of situations (e.g. calculating homotopy and (co)homology groups), this is an apt comparison. But the attaching maps of handles contain considerably more information than cell attachments in CW-complexes, they are usually some kind of generalised knots. Sometimes it is clear how to "discretise" this information, or present it syntactically (e.g. in 2 dimensions), but in general, I don't understand how this could be done.

### Special case: Kirby diagrams

In 4 dimensions, I can imagine a procedure how to describe Kirby diagrams syntactically (by enumerating 1-handles and describing the 2-handle links as braid words), and define the handle cancellations and slides algorithmically. But this feels a bit ad-hoc, and I don't know how it generalises.

## Question

Is there work describing handle decompositions in a detailed manner as a computational model? In particular, I'm looking not just for ad-hoc implementations to do some computations (I know of software to study PL isomorphism and such things in 3d), but rather a clean, general, abstract theory, ideally formally verified (as far as possible).

## Notes

Possibly related: Simplicial complexes are to PL structures of manifolds as simplicial sets are to what?