K. Dosen, Z. Petric
This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
This paper gives a simple presentation of the free star-autonomous category over a category, based on Eilenberg-Kelly-MacLane graphs and Trimble rewiring, yielding a full coherence theorem: the commutativity of diagrams of canonical maps is decidable.
The notion of proof-net category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit free fragment of the notion of star-autonomous categ…
Coherence with respect to Kelly-Mac Lane graphs is proved for categories that correspond to the multiplicative fragment without constant propositions of classical linear first-order predicate logic without or with mix. To obtain this result, coherence is first established for categories that correspond to the multiplicative conjunction-disjunction fragment with first-order quantifiers of classical linear logic, a fragment lacking negation. These results extend results published in previous two books by the authors, where coherence was established for categories of the corresponding fragments o…
A coherence result for symmetric monoidal closed categories with biproducts is shown in this paper. It is explained how to prove, by using the same technique, coherence for compact closed categories with biproducts and for dagger compact closed categories with dagger biproducts.
We introduce homotopical methods based on rewriting on higher-dimensional categories to prove coherence results in categories with an algebraic structure. We express the coherence problem for (symmetric) monoidal categories as an asphericity problem for a track category and we use rewriting methods on polygraphs to solve it. The setting is extended to more general coherence problems, seen as 3-dimensional word problems in a track category, including the case of braided monoidal categories.
It is proved that MacLane's coherence results for monoidal and symmetric monoidal categories can be extended to some other categories with multiplication; namely, to relevant, affine and cartesian categories. All results are formulated in terms of natural transformations equipped with ``graphs'' (g-natural transformations), and corresponding morphism theorems are given as consequences. Using these results, some basic relations between the free categories of these classes are obtained.
Coherence is here demonstrated for sesquicartesian categories, which are categories with nonempty finite products and arbitrary finite sums, including the empty sum, where moreover the first and the second projection from the product of the initial object with itself are the same. (Every bicartesian closed category, and, in particular, the category Set, is such a category.) This coherence amounts to the existence of a faithful functor from categories of this sort freely generated by sets of objects to the category of relations on finite ordinals, and it yields a very easy decision procedure fo…
Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It is found that with the simplest understanding of coherence this is the best on…
A survey is given of results about coherence for categories with finite products and coproducts. For these results, which were published previously by the authors in several places, some formulations and proofs are here corrected, and matters are updated. The categories investigated in this paper formalize equality of proofs in classical and intuitionistic conjunctive-disjunctive logic without distribution of conjunction over disjunction.
Frobenius monoidal functors preserve duals. We show that conversely, (co)monoidal functors between autonomous categories which preserve duals are Frobenius monoidal. We apply this result to linearly distributive functors between autonomous categories.
We study the question when a *-autonomous (Mix-)category has a representation as a $*$-autonomous category of a compact one. We prove that necessary and sufficient condition is that weak distributivity maps are monic (or, equivalently epic). For a Mix-category, this condition is, in turn, equivalent to the requirement that Mix-maps be monic (or epic). We call categories satisfying this property torsion-free. An important side result is that torsion-free categories have canonical partial traces.
This paper presents the proof of the coherence theorem for Ann-categories whose set of axioms and original basic properties were given in [9]. Let $$\A=(\A,{\Ah},c,(0,g,d),a,(1,l,r),{\Lh},{\Rh})$$ be an Ann-category. The coherence theorem states that in the category $ \A$, any morphism built from the above isomorphisms and the identification by composition and the two operations $\tx$, $\ts$ only depends on its source and its target. The first coherence theorems were built for monoidal and symmetric monoidal categories by Mac Lane [7]. After that, as shown in the References, there are many res…
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categories as particular cases, and are adapted to mechanized computations. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed…
A symmetric monoidal category is a category equipped with an associative and commutative (binary) product and an object which is the unit for the product. In fact, those properties only hold up to natural isomorphisms which satisfy some coherence conditions. The coherence theorem asserts the commutativity of all linear diagrams involving the left and right unitors, the associator and the braiding. We prove the coherence for symmetric monoidal categories using a homotopical method based on rewriting. For that scope, we detail the con vergence proof of Lafont's string diagram rewriting system wh…
*-Autonomous categories were initially defined by M. Barr to describe a type of duality carried by many monoidal closed categories. Later they were generalised by the current author to include *-autonomous promonoidal categories. Together, these structures under "convolution" product give a clear indication of the usefulness of *-autonomy in quantum mathematics and related areas.
I motivate a variation (due to K. Szlachányi) of monoidal categories called skew-monoidal categories where the unital and associativity laws are not required to be isomorphisms, only natural transformations. Coherence has to be formulated differently than in the well-known monoidal case. In my (to my knowledge new) version, it becomes a statement of uniqueness of normalizing rewrites. I present a proof of this coherence theorem and also formalize it fully in the dependently typed programming language Agda.
We discuss cyclic star-autonomous categories; that is, unbraided star- autonomous categories in which the left and right duals of every object p are linked by coherent natural isomorphism. We settle coherence questions which have arisen concerning such cyclicity isomorphisms, and we show that such cyclic structures are the natural setting in which to consider enriched profunctors. Specifically, if V is a cyclic star-autonomous category, then the collection of V-enriched profunctors carries a canonical cyclic structure. In the case of braided star-autonomous categories, we discuss the correspon…
Coherence for indexed symmetric monoidal categories
本文针对索引对称幺半范畴这一双范畴细化结构，拓展现有相干定理，证明由其定义的双范畴上一大类运算具有典范同构，并引入判定同构存在性的严格图形演算。
Coherence theorems are fundamental to how we think about monoidal categories and their generalizations. In this paper we revisit Mac Lane's original proof of coherence for monoidal categories using the Grothendieck construction. This perspective makes the approach of Mac Lane's proof very amenable to generalization. We use the technique to give efficient proofs of many standard coherence theorems and new coherence results for bicategories with shadow and for their functors.
This paper proves coherence results for categories with a natural transformation called \emph{intermutation} made of arrows from $(A\wedge B)\vee(C\wedge D)$ to ${(A\vee C)\wedge(B\vee D)}$, for $\wedge$ and $\vee$ being two biendofunctors. Intermutation occurs in iterated, or $n$-fold, monoidal categories, which were introduced in connection with $n$-fold loop spaces, and for which a related, but different, coherence result was obtained previously by Balteanu, Fiedorowicz, Schw\" anzl and Vogt. The results of the present paper strengthen up to a point this previous result, and show that two-f…
We prove coherence theorems for bicategories, pseudofunctors and pseudonatural transformations. These theorems boil down to proving the coherence of some free $(4,2)$-categories. In the case of bicategories and pseudofunctors, existing rewriting techniques based on Squier's Theorem allow us to conclude. In the case of pseudonatural transformations this approach only proves the coherence of part of the structure, and we use a new rewriting result to conclude. To this end, we introduce the notions of white-categories and partial coherence.
The usual coherence theorem of MacLane for categories with multiplication assumes that a certain pentagonal diagram commutes in order to conclude that associativity isomorphisms are well defined in a certain practical sense. The practical aspects include creating associativity isomorphisms from a given one by tensoring with the identity on either the right or the left. We show, by reinspecting MacLane's original arguments, that if tensoring with the identity is restricted to one side, then the well definedness of constructed isomorphisms follows from naturality only, with no need of the commut…
It is known that the quantale of sup-preserving maps from a complete lattice to itself is a Frobenius quantale if and only if the lattice is completely distributive. Since completely distributive lattices are the nuclear objects in the autonomous category of complete lattices and sup-preserving maps, we study the above statement in a categorical setting. We introduce the notion of Frobenius structure in an arbitrary autonomous category, generalizing that of Frobenius quantale. We prove that the monoid of endomorphisms of a nuclear object has a Frobenius structure. If the environment category i…
Local coherence and recollement of abelian categories
本文研究阿贝尔范畴局部相干性在粘合下的传递条件，引入拟射影伴随函子对，推广相干准则，将Stenström的刻画扩展到紧组装Grothendieck范畴，汇集环相干性的等价条件。
It is shown that coherence conditions for monoidal categories concerning associativity are analogous to coherence conditions for symmetric or braided strictly monoidal categories, where associativity arrows are identities. Mac Lane's pentagonal coherence condition for associativity is decomposed into conditions concerning commutativity, among which we have a condition analogous to naturality and a degenerate case of Mac Lane's hexagonal condition for commutativity. This decomposition is analogous to the derivation of the Yang-Baxter equation from Mac Lane's hexagon and the naturality of commut…
Given an additive equational category with a closed symmetric monoidal structure and a potential dualizing object, we find sufficient conditions that the category of topological objects over that category has a good notion of full subcategories of strong and weakly topologized objects and show that each is equivalent to the chu category of the original category with respect to the dualizing object.
A new, self-contained, proof of a coherence result for categories equipped with two symmetric monoidal structures bridged by a natural transformation is given. It is shown that this coherence result is sufficient for $ω\timesω$-indexed family of iterated reduced bar constructions based on such a category.
Given an algebraic theory which can be described by a (possibly symmetric) operad $P$, we propose a definition of the \emph{weakening} (or \emph{categorification}) of the theory, in which equations that hold strictly for $P$-algebras hold only up to coherent isomorphism. This generalizes the theories of monoidal categories and symmetric monoidal categories, and several related notions defined in the literature. Using this definition, we generalize the result that every monoidal category is monoidally equivalent to a strict monoidal category, and show that the "strictification" functor has an i…
We define a traced pseudomonoid as a pseudomonoid in a monoidal bicategory equipped with extra structure, giving a new characterisation of Cauchy complete traced monoidal categories as algebraic structures in Prof, the monoidal bicategory of profunctors. This enables reasoning about the trace using the graphical calculus for monoidal bicategories, which we illustrate in detail. We apply our techniques to study traced ∗-autonomous categories, proving a new equivalence result between the left ⊗-trace and the right ⅋-trace, and describing a new condition under which traced ͨ…
In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible. The presence of a monoidal structure in these categories is not required. We construct several equivalent presentations of the free skew prounital closed category on a given set of generating objects: a categorical calculus (Hilbert-style system), a cut-free sequent calculus a…
Categories of polymorphic lenses in computer science, and of open games in compositional game theory, have a curious structure that is reminiscent of compact closed categories, but differs in some crucial ways. Specifically they have a family of morphisms that behave like the counits of a compact closed category, but have no corresponding units; and they have a `partial' duality that behaves like transposition in a compact closed category when it is defined. We axiomatise this structure, which we refer to as a `teleological category'. We precisely define a diagrammatic language suitable for th…
We study what happens when coherence fails. Categories with a tensor product and a natural associativity isomorphism that does not necessarily satisfy the pentagon coherence requirements (called associative categories) are considered. Categorical versions of associahedra where naturality squares commute and pentagons do not, are constructed (called Catalan groupoids, $\An$). These groupoids are used in the construction of the free associative category. They are also used in the construction of the theory of associative categories (given as a 2-sketch). Generators and relations are given for th…
String diagrams for Strictification and Coherence
本文提出非严格幺半范畴弦图的生成元与关系表示，证明其正确性，并由此给出Mac Lane严格性定理与相干性定理的新图形证明，支持数字电路与编程语言等应用。
Coherence theorems for covariant structures carried by a category have traditionally relied on the underlying term rewriting system of the structure being terminating and confluent. While this holds in a variety of cases, it is not a feature that is inherent to the coherence problem itself. This is demonstrated by the theory of iterated monoidal categories, which model iterated loop spaces and have a coherence theorem but fail to be confluent. We develop a framework for expressing coherence problems in terms of term rewriting systems equipped with a two dimensional congruence. Within this fram…
In this paper we give sufficient conditions for lifting an enhanced factorization system $ (\mathcal{E}, \mathcal{M}) $ on a $ 2 $-category $ \mathbf{D} $ to the functor $ 2 $-category $ \mathbf{D}^{\mathbf{C}} $, where $ \mathbf{C} $ is a small $ 2 $-category. Due to previous work of Lack, our work provides coherence results for $ 2 $-monads on functor $ 2 $-categories. These coherence results are of immediate interest to an ongoing collaboration of Guillou, May, Merling, and Osorno on equivariant infinite loop space theory.
2-Theories are a canonical way of describing categories with extra structure. 2-theory-morphisms are used when discussing how one structure can be replaced with another structure. This is central to categorical coherence theory. We place a Quillen model category structure on the category of 2-theories and 2-theory-morphisms where the weak equivalences are biequivalences of 2-theories. A biequivalence of 2-theories (Morita equivalence) induces and is induced by a biequivalence of 2-categories of algebras. This model category structure allows one to talk of the homotopy of 2-theories and discuss…
Traced monoidal categories as algebraic structures in $\mathbf{Prof}$
本研究提出迹伪幺半群的定义，给出柯西完备迹幺半范畴在$\u003cmath\u003e\mathbf{Prof}\u003c/math\u003e$中的新代数刻画，可借助图形演算推理迹，并将其用于研究迹$*$-自守范畴，得到迹的等价结果与范畴自守的新条件。
Unbiasing symmetric monoidal categories in Lean
本文在Lean 4中形式化了对称单子范畴的去偏过程，通过扩展数据到伪函子并利用Kleisli双范畴实现高 arity张量积的一致性。
Toy models have been used to separate important features of quantum computation from the rich background of the standard Hilbert space model. Category theory, on the other hand, is a general tool to separate components of mathematical structures, and analyze one layer at a time. It seems natural to combine the two approaches, and several authors have already pursued this idea. We explore *categorical comprehension construction* as a tool for adding features to toy models. We use it to comprehend quantum propositions and probabilities within the basic model of finite-dimensional Hilbert spaces.…
We develop an alternative approach to star-autonomous comonads via linearly distributive categories. It is shown that in the autonomous case the notions of star-autonomous comonad and Hopf comonad coincide.
Rewriting techniques for relative coherence
该研究拓展代数结构相干性的重写证明方法，覆盖部分相干性与笛卡尔结构两类情形，构建抽象及项重写系统层面的重写技术与定理，可推导幺半范畴等的相干定理。
We define strict and weak duality involutions on 2-categories, and prove a coherence theorem that every bicategory with a weak duality involution is biequivalent to a 2-category with a strict duality involution. For this purpose we introduce "2-categories with contravariance", a sort of enhanced 2-category with a basic notion of "contravariant morphism", which can be regarded either as generalized multicategories or as enriched categories. This enables a universal characterization of duality involutions using absolute weighted colimits, leading to a conceptual proof of the coherence theorem.
This article tackles categorical coherence within a two-dimensional generalization of Lawvere's functorial semantics. 2-theories, a syntactical way of describing categories with structure, are presented. From the perspective here afforded, many coherence results become simple statements about the quasi-Yoneda lemma and 2-theory-morphisms. Given two 2-theories and a 2-theory-morphism between them, we explore the induced relationship between the corresponding 2-categories of algebras. The strength of the induced quasi-adjoints are classified by the strength of the 2-theory-morphism. These quasi-…
We introduce categorical models of $N_\infty$ spaces, which we call normed symmetric monoidal categories (NSMCs). These are ordinary symmetric monoidal categories equipped with compatible families of norm maps, and when specialized to a particular class of examples, they reveal a connection between the equivariant symmetric monoidal categories of Guillou-May-Merling-Osorno and those of Hill-Hopkins. We also give an operadic interpretation of the Mac Lane coherence theorem and generalize it to include NSMCs. Among other things, this theorem ensures that the classifying space of a NSMC is a $N_\…
An alternative description of symmetric monoidal categories, and symmetric 2-groups
本文提出了一种对称单子族的等价描述，通过结合-交换同构代替传统的结合子和交换子同构，并利用埃利恩伯格-麦克拉伦立方上同调对称2-群进行上同调分类。
Hypergraph categories have been rediscovered at least five times, under various names, including well-supported compact closed categories, dgs-monoidal categories, and dungeon categories. Perhaps the reason they keep being reinvented is two-fold: there are many applications---including to automata, databases, circuits, linear relations, graph rewriting, and belief propagation---and yet the standard definition is so involved and ornate as to be difficult to find in the literature. Indeed, a hypergraph category is, roughly speaking, a "symmetric monoidal category in which each object is equipped…
We study the question when a $*$-autonomous Mix-category has a representation as a $*$-autonomous Mix-subcategory of a compact one. We define certain partial trace-like operation on morphisms of a Mix-category, which we call a mixed trace, and show that any structure preserving embedding of a Mix-category into a compact one induces a mixed trace on the former. We also show that, conversely, if a Mix-category ${\bf K}$ has a mixed trace, then we can construct a compact category and structure preserving embedding of ${\bf K}$ into it, which induces the same mixed trace. Finally, we find a specif…
We introduce and study Hopf monads on autonomous categories (i.e., monoidal categories with duals). Hopf monads generalize Hopf algebras to a non-braided (and non-linear) setting. Indeed, any monoidal adjunction between autonomous categories gives rise to a Hopf monad. We extend many fundamental results of the theory of Hopf algebras (such as the decomposition of Hopf modules, the existence of integrals, Maschke's criterium of semisimplicity, etc...) to Hopf monads. We also introduce and study quasitriangular and ribbon Hopf monads (again defined in a non-braided setting).
In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the resulting type theory to prove a coherence result for cartesian closed bicategories. Cartesian closed bicategories---2-categories `up to isomorphism' equipped with similarly weak products and exponentials---arise in logic, categorical algebra, and game semantics. I show that there is at most one 2-cell between any parallel pair of 1-cells in the free cartesian closed bicategory on a set and hence---in terms of the dif…
Tangent categories were introduced by Rosicky as a categorical setting for differential structures in algebra and geometry; in recent work of Cockett, Crutwell and others, they have also been applied to the study of differential structure in computer science. In this paper, we prove that every tangent category admits an embedding into a representable tangent category---one whose tangent structure is given by exponentiating by a free-standing tangent vector, as in, for example, any model of Kock and Lawvere's synthetic differential geometry. The key step in our proof uses a coherence theorem fo…
Lifting star-autonomous structures
本文研究从基范畴到 Grothendieck 范畴提升星自守结构的条件，推广了松弛自然变换对应工具，并给出通过 $SLatt$ 分解和双重否定核构造星自守范畴的方法，广泛推广了 Hyland 和 Schalk 的正交结构构造。
Topological proofs of categorical coherence
本研究利用单连通CW复形1-骨架等拓扑工具给出范畴化非对称操作子和对称幺半范畴Mac Lane一致性定理的拓扑证明，提出组合同伦概念并结合多面体复形得到几何证明，用Morse理论比较两种方法的普适性，探讨向高范畴推广的可能。
We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a coherator. The coherator encodes all operations required to be present in an ω-category: both the compositions of pasting schemes as well as their coherences. Our main contribution is to provide a ca…
General coherence theorems are constructed that yield explicit presentations of categorical and algebraic objects. The categorical structures involved are finitary discrete Lawvere 2-theories, though they are approached within the language of term rewriting theory. Two general coherence theorems are obtained. The first applies to terminating and confluent rewriting 2-theories. This result is exploited to construct systematic presentations for the higher Thompson groups and the Higman-Thompson groups. The presentations are categorically interesting as they arise from higher-arity analogues of t…
We study integrals of Hopf monoids in duoidal endohom categories of naturally Frobenius map monoidales in monoidal bicategories. We prove two Maschke type theorems, relating the separability of the underlying monoid and comonoid, respectively, to the existence of normalized integrals. It covers the examples provided by Hopf monoids in braided monoidal categories, weak Hopf algebras, Hopf algebroids over central base algebras, Hopf monads on autonomous monoidal categories and Hopf categories.
After recalling basic definitions and constructions for a finite group $G$ action on a $k$-linear category we give a concise proof of the following theorem of Elagin: if $\mathcal{C} = \langle \mathcal{A}, \mathcal{B} \rangle$ is a semiorthogonal decomposition of a triangulated category which is preserved by the action of $G$, and $\mathcal{C}^G$ is triangulated, then there is a semiorthogonal decomposition $\mathcal{C}^G = \langle \mathcal{A}^G, \mathcal{B}^G \rangle$. We also prove that any $G$-action on $\mathcal{C}$ is weakly equivalent to a strict $G$-action which is the analog of the Coh…
A useful general concept of bialgebroid seems to be resolving itself in recent publications; we give a treatment in terms of modules and enriched categories. We define the term "quantum category". The definition of antipode for a bialgebroid is less resolved in the literature. Our suggestion is that the kind of dualization occurring in Barr's star-autonomous categories is more suitable than autonomy (= compactness = rigidity). This leads to our definition of quantum groupoid intended as a "Hopf algebra with several objects".
Statistical models as natural transformations: meaningfulness, coherence and priors as states in Markov categories
本文证明统计模型是设计范畴到Stoch范畴函子间的自然变换，提出有意义性与相干性概念，并揭示岭回归作为高斯线性模型关于高斯先验的贝叶斯反演。
ViCAR: Visualizing Categories with Automated Rewriting in Coq
ViCAR 是一个 Coq 库，提供幺半范畴定义、一致性验证、引理策略及字符串图可视化，支持图形化推理与自动重写。
Kernel theorems for rigidly-compactly generated $\infty$-categories
针对刚性紧生成 $\infty$-范畴及其函子，证明两个表示性定理，将完美对象与（伪）相干对象之间的线性函子用（伪）相干对象或完美对象表示，并应用于谱、概形和Grothendieck对偶。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。