Metacat: a categorical framework for formal systems
Hellas AI
本文提出一个形式系统的范畴框架，通过在cartesian PROP范畴中用特定操作表示蕴含规则，实现元变量上下文的编码，并提供证明检查算法和开源实现。
2026-04-09 cs.LO math.CT
Right-preordered groups from a categorical perspective
本文从范畴论角度研究右预序群，刻画其极限、余极限、正合性与分裂扩张，并指出其范畴与幺半群范畴的相似性及有序群半直积的自然右预序。
2024-06-14 math.CT
Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT
使用依赖类型论来形式化依赖类型论的句法是一个非常活跃的研究课题，并被称为“类型论吃自己”或“类型论中的类型论”。大多数方法至少是松散地基于Dybjer的带族的范畴（CwF），并带有上下文的类型CON，在其上索引的类型族TY建模类型，等等。这在类型论的版本中工作得很好，其中唯一身份证明（UIP）原则成立。然而，在同伦类型论（HoTT）中，类型论是否“吃自己”并能作为自己的解释者是一个长期存在且经常讨论的公开问题。基本的潜在困难似乎是，在没有UIP的情况下，范畴不适合捕捉类型论。在本文中，我们提出了$\infty$ -含族范畴（$\infty$ -CwF's）的概念.使用的方法，以更高的类别依赖于以前建议的半Segal类型，与一个新的建设的身份取代，允许单价和非单价的变化。类型论的宇宙以及内在化的语法都是模型，尽管后者是初始的仍然是一个猜想。为了避免已知的未解决的问题，构造半单纯型，定义在两级类型论（2LTT）。本文除了介绍$\infty$外，还说明了在没有UIP的类型论中1-范畴的缺点，以及内部高维范畴的困难和途径。
2021-01-30 cs.LO math.CT math.LO
Nakayama functor for coalgebras and a categorical perspective of the integral theory for Hopf algebras
本研究回顾余代数的Nakayama函子的基本性质并介绍其在张量范畴的应用，同时给出带预对极的余拟双代数存在非零余积分的等价条件。
2023-06-14 math.CT math.QA math.RT
Virtual double categories of relations relative to fibrations
Dalhousie University（达尔豪斯大学）
本论文提出一种符合范畴逻辑原则的虚拟双范畴方法，在语义侧将其作为谓词逻辑模型以包含现有框架，在语法侧开发名为FVDblTT的类型理论作为其内部语言。
2026-11-09 math.CT
Bayesian Networks, Markov Networks, Moralisation, Triangulation: a Categorical Perspective
本文从范畴论视角提出贝叶斯网络与马尔可夫网络的转换框架，通过函子模型揭示语法与语义修改的差异。
2025-12-10 cs.AI cs.LO math.CT
Categorical Perspectives on Chemical Reaction Networks
通过范畴论方法揭示化学反应网络的拓扑简化过程是函子性的，并定义了从子范畴到CRN的重构函子，证明了与stoichiometric函子的伴随关系。
2026-04-06 math.AT math.CT
A General Probabilistic Framework in IMALL: A Concrete Categorical Perspective
本文在交换半环上的半模范畴框架下研究量子计算背景下提出的sup类型构造子，证明非确定性析构子可由加权余对角映射建模，为幂集单子不适用的场景提供解释非确定性与概率演算的新方案。
2024-04-12 cs.LO math.CT math.LO
Bicategories, Biequivalence, and Bi-Interpretability
本文通过构造相干理论双范畴与相干范畴双范畴之间的双等价，给出双可解释性的范畴刻画，并利用正合完备化得到两个理论双可解释的充要条件，推广到一阶逻辑常见片段。
2023-07-09 math.CT math.LO
A categorical perspective on extended metric-topological spaces
University of Jyvaskyla（于韦斯屈莱大学）
本文从范畴论视角研究扩展度量-拓扑空间的范畴，证明其双完备性。
2026-01-12 math.CT math.GN math.MG
Trees, graphs and aggregates: a categorical perspective on combinatorial surface topology, geometry, and algebra
以费曼范畴的角度来看，曲面几何的几个关键方面推导出组合结构与图形。这提供了一个直接的路线，从组合的图形字符串拓扑运算，通过拓扑，几何和代数。特别是，列入树到图和解剖图到聚集产生一个简洁的形式主义循环和模块操作，以及他们的多环和表面类型的概括。后者在二维拓扑域论和弦拓扑学中占有突出地位。范畴观点允许我们使用费曼操作的左Kan扩展作为有效的计算工具。计算涉及的结构图，预计将是独立的利益的某些类别的研究。
2022-01-25 math.AG math.AT math.CO
Theory of Interpretations II. Categorical equivalence of projective logical geometries
Sobolev Institute of Mathematics（索博列夫数学研究所）；Stevens Institute of Technology（史蒂文斯理工学院）
该研究引入射影逻辑几何，证明两个代数结构强双可解释的条件是其射影逻辑集范畴或射影可定义集范畴相对于特定函子类等价，推广了相关概念，用范畴方法为解释理论带来新视角并建立基本结果。
2026-07-28 math.CT math.LO
A Categorical Perspective on Gluing
本文在一般范畴中建立粘合数据函子与精细粘合理论，刻画相关锥和极限，并证明拓扑空间范畴上的粘合覆盖构成 Grothendieck 拓扑。
2024-01-18 math.CT
Functorial Approach to Graph and Hypergraph Theory
利用范畴语法和范畴语义为范畴图和超图理论提供了一种新的研究方法。对于每个幺半群$M$和一个集合$X$上的动作，有一个相关的$(X,M)$ -图的预层拓扑，其中每个对象可以被解释为一个广义均匀超图，其中每个边都有基数$\#X$事件顶点（包括多重性），并且幺半群通知边拥有什么类型的凝聚力。$(X,M)$ -图的一个显著特征是存在不固定边。我们证明了，如果一个图或一致超图的指数和有效的等价关系存在的范畴中，不固定的边缘是一个必要的特征。将语法（$(X,M)$ -图论）与语义（$(X,M)$ -图的范畴）分离的主要优点是能够在任何共完备范畴中解释该理论。这个interpetation函子，然后产生一个神经实现的adjunction，并允许我们转移结构之间的类别的$(X,M)$ -图和接受的共完全范畴。
2019-07-04 math.CO math.CT
Adjunctions for exceptions
用代数方法研究计算机语言中异常的语义。异常形成了一种计算效果，在这个意义上，异常的语法和它们预期的语义之间存在明显的不匹配。我们解决了这个明显的矛盾，通过定义一个逻辑的例外与证明系统，这是接近他们的语法和他们的意图语义可以被看作是一个模型。这需要一个强大的逻辑框架和它们的态射，这是由依赖于概念，分数和极限草图的分类工具提供的。
2012-10-27 cs.LO math.CT
A categorical model structure for generalized algebraic theories
该研究在广义代数理论范畴上构造了Quillen模型结构，比较了两类广义代数理论态射，证明了相关严格化结果，并刻画了模型的可严格化性，揭示了其语义行为。
2026-08-31 math.CT math.LO
Gauging Noninvertible Defects: A 2-Categorical Perspective
本文利用2-范畴凝聚框架将对称性反常推广至非可逆对称性，证明了多重融合2-范畴中代数对象凝聚的结构定理，并通过上同调计算找到了进一步凝聚至真空理论的阻碍。
2022-11-25 hep-th math-ph math.CT
A categorical perspective on constraint satisfaction: The wonderland of adjunctions
Charles University, Prague, Czech Republic（布拉格查理大学）；Czech Technical University, Prague, Czech Republic（捷克理工大学）；University of Birmingham, Birmingham, UK（伯明翰大学）
本文从范畴论角度探讨约束满足问题及Promise约束满足问题的复杂性，通过范畴论方法重新证明核心结果，展现更简洁且广泛适用的证明方式，为研究提供新视角。
2026-05-14 cs.LO math.CT
El Teorema de Gelfand Naimark desde una perspectiva Categórica The Gelfand--Naimark Theorem from a Categorical Perspective
本文证明了 Hausdorff-紧致拓扑空间范畴与含幺交换 $C^*$-代数范畴的等价性，将 Gelfand-Naimark 定理重写为范畴论语言，并展示了该视角在解决代数问题中的应用。
2024-09-24 math.CT math.OA
A 3-categorical perspective on G-crossed braided categories
本文从3-范畴的角度，将G-交叉辫子范畴与群G的结构联系起来，提供了一种统一的构造方法。
2020-09-01 math.CT math.QA
A categorical approach to open and interconnected dynamical systems
University of Oxford（牛津大学）；University of Pennsylvania（宾夕法尼亚大学）；University of Southampton（南安普顿大学）
本文提出一种图形理论，用于描述离散线性时不变动态系统，强调非可控系统和可控性的结构特征。
2016-02-02 cs.LO cs.SY eess.SY
The Geometric Completion of a Doctrine
本文提出以Grothendieck拓扑为第二参数的学说几何完备化，证明其幂等且对可表示为连续平坦函子范畴的学说语义不变，并阐明其与其他学说完备化及语法范畴构造的关系。
2023-04-15 math.CT math.LO
Open Systems: A Double Categorical Perspective
Fong开发了“装饰cospans”来模拟各种开放系统：即具有输入和输出的系统。在这个框架中，开放系统被看作是范畴的态射，并且可以这样组成，允许更大的开放系统从更小的系统建立起来。在这个方向上已经做了很多工作，但有一个问题：修饰余跨度之间的同构概念往往限制太多。在这里，我们介绍并比较了两种解决这个问题的方法：结构化的cospans，和一个新版本的装饰cospans。结构化cosspan非常简单：给定一个函子$L \colon \mathsf{A} \to \mathsf{X}$，“结构化cosspan”是$\mathsf{X}$中的一个图，形式为$L(a) \rightarrow x \leftarrow L(b)$。若$\mathsf{A}$和$\mathsf{X}$有有限余极限，且$L$是左伴随，则存在一个对称幺半范畴，其对象是$\mathsf{A}$的对象，其态射是结构余跨距的同构类.然而，这个范畴产生于一个更基本的结构：一个对称的monoidal double范畴。在一定条件下，这个对称monoidal双范畴等价于用我们的新版本的装饰cospans构造的范畴。我们将这些思想应用到对称么半群双范畴的开放电路，开放马尔可夫过程和开放Petri网。
2020-08-05 math.CT
Generalized Inverses of Quantum Channels: a categorical perspective
University of Calgary（卡尔加里大学）；Macquarie University（麦考瑞大学）；Tallinn University of Technology（塔尔图理工大学）
本文从范畴论视角研究量子通道的广义逆，证明Drazin逆始终保迹，并推广至dagger Drazin逆，显示Moore-Penrose逆在保迹和单位性上的应用。
2026-11-05 math.CT quant-ph
A Syntax for Strictly Associative and Unital $\infty$-Categories
本文提出严格结合且含单位的 $\infty$-范畴的首个类型论语法，以 insertion 计算规则保证严格性并获得相等性判定程序，且通过 OCaml 实现与高阶同伦示例验证。
2024-07-04 cs.LO math.CT
No-Cloning In Categorical Quantum Mechanics
最近，作者和Bob Coecke介绍了量子力学的范畴表述。在本文中，我们将用它来开辟一个新的视角，不克隆。我们将发现，相当出乎意料的是，它与逻辑、计算和数学基础中的一些基本问题有联系。我们的结果的一个显着特点是，他们显然是在同一流派的一个著名的结果Joyal在分类逻辑表明，一个布尔carnival闭范畴平凡化，这提供了一个主要的路障经典逻辑的计算解释。事实上，他们加强了Joyal的结果，只要假设一个完整的范畴产品（对角线和投影）在一个经典的对偶性的存在被削弱。这表明了证明论中的限制性结果与量子力学中的No-Go定理之间迄今未被怀疑的联系。
2012-03-19 math.CT math.LO quant-ph
A Categorical Framework for Program Semantics and Semantic Abstraction
本文提出一种用于抽象解释的函子方法，将解释表示为偏序集范畴中的oplax函子，并用lax自然变换表示抽象关系，从而将函子语义的优势引入语义抽象并讨论了其健全性。
2023-11-18 cs.PL math.CT
Circuits, Bond Graphs, and Signal-Flow Diagrams: A Categorical Perspective
我们使用“道具”的框架来研究电路、信号流程图和键合图。Prop是严格对称的幺半范畴，其中对象是自然数，对象的张量积由加法给出。在这种方法中，电路构成了道具中的态射，信号流程图和键合图也是如此。具有$m$输入和$n$输出的网络（例如电路）是从$m$到$n$的态射，而将网络串联在一起是合成，将它们并排设置是张量。在这里，我们为各种电路，然后是信号流程图，然后是键合图制定这种方法的细节。每一种网络对应于一个数学上自然的道具。我们还描述了“行为”的电路，键合图，和信号-流程图使用道具之间的态射。为了将一个行为分配给一个网络，我们对网络进行了“黑盒”处理，它忘记了它的内部工作，只记录了它在输入和输出之间施加的关系。黑盒网络的过程对应于道具之间的态射。有趣的是，任何键合图都有两种不同的行为，它们通过自然变换联系在一起。为了实现这一切，我们首先证明了一些关于道具的基本结果。这些结果让我们可以用生成元和方程来描述任何道具，也可以通过命名生成元的位置并检查相关方程是否成立来定义道具的态射。从技术上讲，关键的工具是Rosebrugh-Sabadini-Walters的结果，将电路与特殊的交换Frobenius幺半群联系起来，道具和签名之间的一元附加，以及一个结果，说明哪些对称的幺半范畴等价于道具。
2018-05-21 math.CT
Knowledge Representation in Bicategories of Relations
Department of Statistics, Stanford University（斯坦福大学统计系）
我们介绍了关系本体日志，或关系日志，一个知识表示系统的基础上的集合和关系的范畴。它的灵感来自Spivak和Kent的olog，一个最近的知识表示的分类框架。关系逻辑介于逻辑和描述逻辑之间，描述逻辑是当今知识表示的主要形式。在本文中，我们调查关系逻辑本身的缘故，并深入了解之间的关系的代数和逻辑方法的知识表示。在实际的层面上，我们通过例子表明，关系日志有一个友好和直观的-但完全精确的-图形语法，来自monoidal类别的字符串图。我们解释了其他几个有用的功能的关系逻辑不具备大多数描述逻辑，如类型系统和丰富的，灵活的概念的实例数据。在一个更理论化的脉络中，我们利用范畴逻辑来展示关系逻辑如何在一阶逻辑的片段中被翻译成逻辑理论。虽然我们大量使用范畴语言，但本文的设计是自成一体的，有相当多的过渡性内容。唯一的先决条件是一阶逻辑的知识和范畴论的雏形。
2017-11-01 cs.AI cs.LO math.CT
A Categorical Perspective on Braid Representations
University of Leeds（利兹大学）；Texas A&M University（德克萨斯农工大学）；University of Bristol（布里斯托大学）；Heilbronn Institute of Mathematics（海尔布隆数学研究所）
本文从范畴论视角研究辫子表示，通过引入函子范畴的幺半结构、子对象与商对象等工具，揭示了电荷守恒 Yang-Baxter 算子分类的范畴机制，并证明了足够自由条件下幺半函子可严格化。
2026-09-28 math.CT math.QA math.RT
Quantum Logic in Dagger Kernel Categories
本文从范畴逻辑的角度研究量子逻辑，从最小假设出发，即对合/匕首和核的存在性。由此产生的结构（1）包含许多感兴趣的例子，如关系的类别，部分注入，希尔伯特空间（也模相位）和布尔代数，（2）具有有趣的分类/逻辑属性，在核纤维化方面，如拉回，因子分解和正交模的存在。例如，Sasaki hook和and-then连接词作为伴随词，通过纤维之间的存在拉回连接而获得。
2009-12-04 math.CT math.LO quant-ph
Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
本文从范畴和代数的角度研究了类型化λ演算的赋值正规化问题。本文的第一部分通过Kripke逻辑关系分析了Jung和Tiuryn的lambda可定义性结果，并展示了它如何适用于统一可定义性和规范化，产生一个扩展的规范化结果。在第二部分的文件的分析进一步细化考虑内涵Kripke关系（在阿丁胶合的形式），并显示提供一个功能的规范化条款，铸造规范化的范畴胶合的背景下进行评估。技术发展包括类型化λ演算的语法和语义的代数处理，其允许在简单类型化元理论内给出规范化函数的定义。合成依赖类型的函数式程序设计语言中的求值规范化程序。
2022-08-18 cs.LO math.CT
A categorical approach to the set-theoretic Yang-Baxter equation
本研究从范畴论视角探究集合论Yang-Baxter方程的解，将现有相关成果重述为范畴论形式以证明部分假设多余，通过识别合适子范畴刻画解并催生新解，还证明Płonka双magma范畴同构于特定子范畴，引入并研究新的Lyubashenko型解。
2026-10-14 math.CT math.QA math.RA
Abstract sheaf theory
本文从范畴的观点研究层理论。这种观点极大地推广了通常的理论层的集合到一个更抽象的设置，使我们能够调查理论层的价值在一个任意的类别。
2017-09-21 math.AC math.CT
t-structures on stable infinity-categories
目前的工作重新制定的经典理论的t-结构减少经典的定义 *Faisceaux Pervers* 到一个相当原始的范畴小工具：合适的反射因子分解系统。这种翻译是唯一可能的，由于无穷范畴设置的优点。一旦t-结构的基本理论得到发展，一个自然的研究方向是在“torsio-centric”的视角下对t-结构进行全面的处理：我们将因子分解系统的技术应用于Postnikov塔理论，证明t-结构的心脏的abelianity，以及Bridgeland稳定条件的理论。
2020-05-28 math.AT math.CT
