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）的态射集合，使得态射可以组合，组合是结合的，并且每个对象对自身有一个恒等态射。尽管有这个相当抽象的定义，但我们经常处理范畴，甚至没有意识到这一点——例如，Set将集合作为对象，将集合之间的函数作为态射，而vetk将域k上的向量空间作为对象，将k-线性映射作为态射。范畴论在计算机科学、物理和数学领域有着广泛的应用，包括函数式编程、量子计算和代数拓扑。在我的研究中，我想把范畴论的工具应用到这些领域。写关于范畴论和同调代数的硕士项目让我对这两个领域产生了浓厚的兴趣，尤其是这两者之间的联系。在阅读了Alu b[1]的《代数：第0章》和Weibel b[6]的《同调代数导论》之后，我想了解更多关于派生范畴及其应用的知识，因为它们在同调代数中具有明显的重要性，并且目前对派生范畴的研究很多。我也对同调镜像对称以及其他（co）同调理论（如k理论）以及如何使用它们来解决物理问题感兴趣。我最近参加了第六届组成结构研讨会（SYCO6），在那里我接触到了许多我以前从未见过的范畴论和图形演算的应用——Vincent Wang关于“图形语法和一元范畴的图形补全”的演讲给我带来了深刻的印象，因为范畴论似乎很自然地应用于语法结构的研究，但我以前从未听说过它在这里被使用。讲座结束后，我发现Bob Coecke关于语言学范畴论的论文非常有趣，我想在我的研究中进一步研究这个问题。除此之外，王全龙关于“zx微积分的代数公理化”的演讲对我来说非常有趣，并帮助我展示了图解推理的使用是多么严格。我想研究的另一个领域是高级范畴理论。最近在同伦理论和理论物理中有许多高范畴论的应用，我发现这些应用非常有趣，并且想要研究一下，然而高范畴通常很难概念化。证明助手可以是非常强大的工具，用于可视化特定类型的n个类别，允许我们研究n个类别，而无需检查所有内容是否符合正确的公理（其中有许多用于更高类别的公理），因为这是由证明助手处理的。我的目标是与证明助手一起工作，比如同伦。发展高范畴理论并研究其在拓扑量子场论中的应用，特别是在3 + 1和更高维度的应用，因为这些还不太清楚。除了更高类别的应用，我也想研究更高类别的不同模型。在n范畴中，对于所有k = 2，不仅存在每对对象之间的态射集，而且存在每对对象之间k1态射的k态射集；3;:::;n;有许多不同的方式可以定义高级态射的组合，使得一般的高级类别难以处理。我计划学习更多关于更高类别的知识，并研究更高类别的哪些模型对物理应用最强大。我对拓扑学很着迷，我试着尽可能多地阅读它；尤其是自从发现范畴论并看到它对代数拓扑学的发展有多么重要之后。我希望能够更多地了解更高范畴在同伦理论中的应用，并在未来进行自己的研究。

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.