scholarly journals Coherence of proof-net categories

2005 ◽  
Vol 78 (92) ◽  
pp. 1-33 ◽  
Author(s):  
Kosta Dosen ◽  
Zoran Petric

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 category, a special kind of symmetric monoidal closed category.

1996 ◽  
Vol 3 (61) ◽  
Author(s):  
Sergei Soloviev

Some sufficient conditions on a Symmetric Monoidal Closed category K are obtained such that a diagram in a free SMC category generated by the set A of atoms commutes if and only if all its interpretations in K are commutative. In particular, the category of vector spaces on any field satisfies these conditions (only this case was considered in the original Mac Lane conjecture). Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent if and only if all their interpretations in K are equal. In fact, the assignment of values (objects of K) to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R. Voreadou's proof of the "abstract coherence theorem" found by the author, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of S. Mac Lane conjecture proves also the correctness of the modified description.


1978 ◽  
Vol 18 (3) ◽  
pp. 357-371 ◽  
Author(s):  
B.J. Day ◽  
M.L. Laplaza

This article contains one method of fully embedding a symmetric closed category into a symmetric monoidal closed category. Such an embedding is very useful in the study of coherence problems. Also we give an example of a non-symmetric closed category for which, under the embedding discussed in this article, the resultant monoidal closed structure has associativity not an isomorphism.


1975 ◽  
Vol 12 (1) ◽  
pp. 49-72 ◽  
Author(s):  
Francis Borceux ◽  
G.M. Kelly

For a V-category B, where V is a symmetric monoidal closed category, various limit-like notions have been recognized: ordinary limits (in the underlying category B0 ) preserved by the V-valued representable functors; cotensor products; ends; pointwise Kan extensions. It has further been recognized that, to be called complete, B should admit all of these; for which it suffices to demand the first two. Hitherto, however, there has been no single limit-notion of which all these are special cases, and particular instances of which may exist even when B is not complete or even cotensored. In consequence it has not been possible even to state, say, the representability criterion for a V-functor T: B → V, or even to define, say, pointwise Kan extensions into B, except for cotensored B. (It is somewhat as if, for ordinary categories, we had the notions of product and equalizer, but lacked that of general limit, and could not discuss pullbacks in the absence of products.) In this paper we provide such a general limit-notion for V-categories.


1978 ◽  
Vol 18 (1) ◽  
pp. 125-135
Author(s):  
Francis Borceux ◽  
B.J. Day

The aim of this article is to characterise categories which are V–algebraic (equals V–theoretical) over V where V is a symmetric monoidal closed category satisfying suitable limit-colimit commutativity conditions (basicly axiom π).


1975 ◽  
Vol 19 (2) ◽  
pp. 180-195 ◽  
Author(s):  
Harvey Wolff

Kock (1970) defined the notion of a commutative monad in a symmetric monoidal closed category V and in Kock (1971) showed that the algebras for such a monad had a canonical structure as a closed category and that the monad had a canonical closed structure. In this paper we are concerned with the relationship between distributive laws and commutivity. In particular, the following question arises: given a distributive law between two monads on V when is the composite monad commutatice? To answer this question we define commutative distributive laws and show that if the composite is commutative then the distributiove law must be commutative. We also show that if Y and J are commutative monads in V with a commutative distributive law between them then the composite is commutative. So we get that if Y and J are commutative then the composite is commutative if and only if the distributive law is commutative. In addition we show that if the monads and the distributive law are commutative then the lifting of the monad Y to the category of J-algebras has a canonical structure as a closed monad (closed relative to the canonical closed category structure on the J algebras).


1970 ◽  
Vol 3 (3) ◽  
pp. 375-383 ◽  
Author(s):  
H. Wiesler ◽  
G. Calugareanu

Let v be a symmetric monoidal closed category with equalizers. The v–triples T, T′, … in the enriched category A, together with suitably defined morphisms form a category v–Trip(A). The v–categories AT, AT′, … and the v–functors R: AT′ → AT which are compatible with the forgetful functors form a category V–Alg(A).In the subsequent note it is shown that V–Trip(A) is isomorphic to the dual of V–Alg(A) and that the morphisms of V–Alg(A) are inverse limit preserving V–functors.


2007 ◽  
pp. 17-23
Author(s):  
Kosta Dosen ◽  
Zoran Petric

A relevant category is a symmetric monoidal closed category with a diagonal natural transformation that satisfies some coherence conditions. Every cartesian closed category is a relevant category in this sense. The denomination relevant comes from the connection with relevant logic. It is shown that the category of sets with partial functions, which is isomorphic to the category of pointed sets, is a category that is relevant, but not cartesian closed.


1978 ◽  
Vol 19 (3) ◽  
pp. 445-456 ◽  
Author(s):  
B.J. Day

Let V denote the symmetric monoidal closed category of limit-space abelian groups and let L denote the full subcategory of locally compact Hausdorff abelian groups. Results of Samuel Kaplan on extension of characters to products of L–groups are used to show that each closed subgroup of a product of L-groups is a limit of L–groups. From this we deduce that the limit closure of L in V is reflective in V and has every group Pontryagin reflexive with respect to the structure of continuous convergence on the character groups. The basic duality L ≃ Lop is then extended.


1993 ◽  
Vol 3 (2) ◽  
pp. 259-276 ◽  
Author(s):  
Guo-Qiang Zhang

This paper introduces the following new constructions on stable domains and event structures: the tensor product; the linear function space; and the exponential. These give rise to a monoidal closed category of dI-domains and to stable event structures, which can be used to interpret intuitionistic linear logic. Finally, the usefulness of the category of stable event structures for modeling concurrency and its relation to other models are discussed.


2016 ◽  
Vol 10 (02) ◽  
pp. 1750037
Author(s):  
Farideh Farsad ◽  
Halimeh Moghbeli-Damaneh

In this paper, we consider the category Dcpo-S of [Formula: see text]-dcpos and [Formula: see text]-dcpo maps between them. This category is enriched over the symmetric monoidal closed category Dcpo. So, we are going to find weighted limits in this category. In fact, we show that the category of [Formula: see text]-dcpos has weighted limits. Finally, we give a concrete construction of some kinds of weighted limits in this category.


Sign in / Sign up

Export Citation Format

Share Document