In this talk, I will present my PhD work on enhancing the combinatorial foundation of the proof assistant homotopy.io to support invertible generators.
The theory of associative n-categories has been employed to give a combinatorial model of directed higher categories amenable to computer implementation, presented as n-dimensional string diagrams. However, the theory lacks a notion of inverse, which would require the existence of cancellation moves along with an infinite collection of higher-dimensional coherence data.
We generalise the theory to support invertibility by equipping generators with framing data, allowing for a natural representation of the inverse. Using this framed zigzags approach, we show that the required cancellation moves and coherence data arise uniformly via a colimit mechanism. We use tools from enriched category theory to justify correctness of our constructions, and exhibit a proof assistant which implements our theory.