Cartesian Differential Categories as Skew Enriched Categories

We exhibit the cartesian differential categories of Blute, Cockett and Seely as a particular kind of enriched category. The base for the enrichment is the category of commutative monoids—or in a straightforward generalisation, the category of modules over a commutative rig k. However, the tensor product on this category is not the usual one, but rather a warping of it by a certain monoidal comonad Q. Thus the enrichment base is not a monoidal category in the usual sense, but rather a skew monoidal category in the sense of Szlachányi. Our first main result is that cartesian differential categories are the same as categories with finite products enriched over this skew monoidal base. The comonad Q involved is, in fact, an example of a differential modality. Differential modalities are a kind of comonad on a symmetric monoidal k-linear category with the characteristic feature that their co-Kleisli categories are cartesian differential categories. Using our first main result, we are able to prove our second one: that every small cartesian differential category admits a full, structure-preserving embedding into the cartesian differential category induced by a differential modality (in fact, a monoidal differential modality on a monoidal closed category—thus, a model of intuitionistic differential linear logic). This resolves an important open question in this area.

Weighted limits in the category Dcpo-S

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.

On traced monoidal closed categories

The structure theorem of Joyal, Street and Verity says that every traced monoidal category arises as a monoidal full subcategory of the tortile monoidal category Int. In this paper we focus on a simple observation that a traced monoidal category is closed if and only if the canonical inclusion from into Int has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts for traced models of linear logic, and some for models of fixed-point computation. To make the paper more self-contained, we also include various background results for traced monoidal categories.

Completions of Non-Symmetric Metric Spaces Via Enriched Categories

It is known from [Lawvere, Repr. Theory Appl. Categ. 1: 1–37 2002] that nonsymmetric metric spaces correspond to enrichments over the monoidal closed category [0, ∞]. We use enriched category theory and in particular a generic notion of flatness to describe various completions for these spaces. We characterise the weights of colimits commuting in the base category [0, ∞] with the conical terminal object and cotensors. Those can be interpreted in metric terms as very general filters, which we call filters of type 1. This correspondence extends the one between minimal Cauchy filters and weights which are adjoint as modules. Translating elements of enriched category theory into the metric context, one obtains a notion of convergence for filters of type 1 with a related completeness notion for spaces, for which there exists a universal completion. Another smaller class of flat presheaves is also considered both in the context of both metric spaces and preorders. (The latter being enrichments over the monoidal closed category 2.) The corresponding completion for preorders is the so-called dcpo completion.

Relevant categories and partial functions

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.

Coherence of proof-net categories

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.

Isomorphic objects in symmetric monoidal closed categories

This paper presents a new and self-contained proof of a result characterizing objects isomorphic in the free symmetric monoidal closed category, i.e., objects isomorphic in every symmetric monoidal closed category. This characterization is given by a finitely axiomatizable and decidable equational calculus, which differs from the calculus that axiomatizes all arithmetical equalities in the language with 1, product and exponentiation by lacking 1c=1 and (a · b)c =ac · bc (the latter calculus characterizes objects isomorphic in the free cartesian closed category). Nevertheless, this calculus is complete for a certain arithmetical interpretation, and its arithmetical completeness plays an essential role in the proof given here of its completeness with respect to symmetric monoidal closed isomorphisms.

Proof of a Conjecture of S. Mac Lane

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.

Enriched accessible categories

We consider category theory enriched in a locally finitely presentable symmetric monoidal closed category ν. We define the ν-filtered colimits as those colimits weighted by a ν-flat presheaf and consider the corresponding notion of ν-accessible category. We prove that ν-accessible categories coincide with the categories of ν-flat presheaves and also with the categories of ν-points of the categories of ν-presheaves. Moreover, the ν-locally finitely presentable categories are exactly the ν-cocomplete finitely accessible ones. To prove this last result, we show that the Cauchy completion of a small ν-category Cis equivalent to the category of ν-finitely presentable ν-flat presheaves on C.