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

范畴理论是对数学结构的研究-范畴C由一类对象Obj(C)组成，对于每两个对象A；B2Obj(C)，有一组态射HomC(A；B)，使得态射可以合成，合成是结合的，并且每个对象本身都有一个恒等态射。尽管有这种相当抽象的定义，但人们经常处理范畴，甚至没有意识到这一点--例如，集合将集合作为对象，集合之间的函数作为态射，而Vectk将域k上的向量空间作为对象，将k-线性映射作为态射。范畴理论在计算机科学、物理和数学中有着广泛的应用，包括在函数编程、量子计算和代数拓扑学中。在我的研究过程中，我想把范畴理论的工具应用到这些领域。在写我的范畴理论和同调代数的硕士论文时，我对这两个领域都产生了浓厚的兴趣，特别是对两者之间的相互联系。在阅读了Alu[1]的《代数：0章》和Webel[6]的《同调代数导论》之后，我想更多地了解派生范畴及其应用，因为它们在同调代数中具有明显的重要性，而且目前对派生范畴的研究也很多。我还对同调镜像对称性以及其他(共)同调理论，如K-理论以及如何用它们来解决物理问题感兴趣。我最近参加了第六届组成结构研讨会(SYCO6)，在会上我被介绍到了许多我以前没有见过的范畴理论和图形演算的应用--文森特·王关于图形语法和一元式范畴的图形完成的演讲对我来说很突出，因为范畴理论似乎很自然地用于语法结构的研究，但我以前没有听说过它在这里被用过。自那次演讲以来，我发现鲍勃·科克关于语言学范畴理论的论文非常有趣，我想在我的研究中进一步探讨这一点。此外，王全龙关于ZX-演算的代数公理化的演讲对我来说非常有趣，并帮助我展示了图解推理的使用是多么严格。我想要研究的另一个领域是更高范畴理论。最近，更高范畴理论在同伦理论和理论物理中的许多应用，我发现非常有趣，并想研究一下，然而更高范畴通常很难概念化。证明助手可以是非常强大的工具，用于可视化特定类型的n-范畴，允许我们研究n-范畴，而不必检查一切是否都符合正确的公理(对于更高的范畴，有许多公理)，因为这是由证明助手处理的。我的目标是与Homotopy.io这样的证明助手合作，发展更高范畴理论，并研究它在拓扑量子场论中的应用，特别是在3+1维和更高维度，因为这些还不被很好地理解。除了更高范畴的应用，我还想研究更高范畴的不同模型。在n-范畴中，不仅在每对对象之间存在态射集合，而且对于所有k=2；3；：：；n，在每对k1态射之间存在k-态射集合；有许多不同的方法可以定义更高的态射的合成，使得一般的更高的范畴难以处理。我计划学习更多关于更高类别的知识，并研究哪些更高类别的模型对于物理应用最强大。我一直对拓扑学着迷，并尽可能多地阅读有关它的书籍；特别是在发现范畴理论并看到它对代数拓扑学最近的发展是多么重要之后。我希望能够学习更多关于更高范畴在同伦理论中的应用的知识，并在未来对其进行自己的研究。

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.