Graphical calculi and proof assistants in monoidal n-categories and their application to topological quantum field theory.

Category theory is the study of mathematical structure - a category C consists of a class of objects Obj(C) and, for every two objects A;B 2 Obj(C), a set HomC(A;B) of morphisms such that morphisms can be composed, composition is associative, and every object has an identity morphism to itself. Despite this rather abstract denition, one deals with categories regularly even without realising so - for example, Set has sets as objects and functions between sets as morphisms, while Vectk has vector spaces over a field k as objects and k-linear maps as morphisms. Category theory has a wide range of applications across computer science, physics and maths, including in functional programming, quantum computing and algebraic topology. I would like to apply tools from category theory to these areas during my research. Writing my master's project on category theory and homological algebra has led me to develop a strong interest in both areas, and especially with the interconnections between the two. After reading Algebra: Chapter 0 by Alu[1] and An introduction to homological algebra by Weibel [6] I would like to learn more about derived categories and their applications as they are of obvious importance in homological algebra and there is much current research on derived categories. I am also interested in Homological mirror symmetry as well as other (co)homology theories such as K-theory and how they may be used to solve physical problems.

I recently attended the Sixth Symposium on Compositional Structures (SYCO6) where I was introduced to many applications of category theory and graphical calculi which I had not seen before - Vincent Wang's talk on \Graphical Grammar and Graphical Completion of Monoidal Categories" stood out to me as category theory seems natural to use in the study of grammatical structures, yet I had not previously heard of it being used here. Since the talk I have found Bob Coecke's papers on category theory in linguistics very interesting and would like to look further into this during my research. As well as this, Quanlong Wang's talk on \An algebraic axiomatisation of ZX-calculus" was very interesting to me and helped to show me how rigorous the use of diagramatic reasoning can be.

Another area I would like to do research in is higher category theory. There are many recent applications of higher category theory in homotopy theory as well as theoretical physics which I have found very interesting and would like to look into, however higher categories are often hard to conceptualise. Proof assistants can be very powerful tools for visualising specific types of n-categories, allowing us to study n-categories without having to check that everything obeys the correct axioms (of which there are many for higher categories) as this is handled by the proof assistant. I aim to work with proof assistants such as homotopy.io to develop higher category theory and to study its applications intopological quantum field theory, specially in dimensions 3 + 1 and higher as these are less well understood.

As well as applications of higher categories, I would also like to research different models of higher categories. In an n-category, there are not only sets of morphisms between each pair of objects, but also sets of k-morphisms between each pair of k1 morphisms for all k = 2; 3; :::; n; there are many different ways the composition of higher morphisms may be defined, making general higher categories hard to deal with. I plan to learn more about higher categories and to study which models of higher categories are the most powerful for physical applications. I have been fascinated with topology and I have tried to read as much as I can on it; especially since discovering category theory and seeing how important has been for recent developments in algebraic topology. I would like to be able to learn more about application of higher categories to homotopy theory and to do my own research into it in the future.