Automated rewriting for higher categories and applications to quantum theory

Thesis

The contribution of this thesis is a novel framework for rewriting in higher categories. Its theoretical foundation is the theory of quasistrict higher categories and the practical realisation is a proof assistant Globular. The framework introduces the notions of diagrams and signatures as new mutually-recursive structures that give the algebraic basis for the approach. These structures are related the notion of an n-polygraph, but allow reasoning about quasistrict higher categorical structures in a way amenable to computer implementation. Building on this, we propose a new definition of a quasistrict 4-category, and prove a result that in a quasistrict 4-category, an adjunction of 1-morphisms gives rise to a coherent adjunction satisfying the butterfly equations.

Authors: Bar, K

• DOI: 10.5287/ora-bpjzpkxqo
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Subjects: Categories (Mathematics); Quantum theory