# Categorical semantics

Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.

TODO: why categories? how to extract categorical models? etc.

See ^{[1]}for a more detailed introduction to category theory. See ^{[2]}for a detailed treatment of categorical semantics of linear logic.

## Contents |

## Basic category theory recalled

**Definition** (Category)

**Definition** (Functor)

**Definition** (Natural transformation)

**Definition** (Adjunction)

**Definition** (Monad)

## Overview

In order to interpret the various fragments of linear logic, we define incrementally what structure we need in a categorical setting.

- The most basic underlying structure are
**symmetric monoidal categories**which model the symmetric tensor and its unit 1. - The fragment (IMLL) is captured by so-called
**symmetric monoidal closed categories**. - Upgrading to ILL, that is, adding the exponential modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough
**adjunctions**, or with an ad-hoc definition of a well-behaved comonad which leads to**linear categories**and close relatives. - Dealing with the additives is quite easy, as they are plain
**cartesian product**and**coproduct**, usually defined through universal properties in category theory. - Retrieving , and is just a matter of dualizing , 1 and , thus requiring the model to be a
***-autonomous category**for that purpose.

## Modeling IMLL

A model of IMLL is a *closed symmetric monoidal category*. We recall the definition of these categories below.

**Definition** (Monoidal category)

A *monoidal category* is a category equipped with

- a functor called
*tensor product*, - an object
*I*called*unit object*, - three natural isomorphisms α, λ and ρ, called respectively
*associator*,*left unitor*and*right unitor*, whose components are

such that

- for every objects
*A*,*B*,*C*,*D*in , the diagram

commutes,

- for every objects
*A*and*B*in , the diagram

commutes.

**Definition** (Braided, symmetric monoidal category)

A *braided* monoidal category is a category together with a natural isomorphism of components

called *braiding*, such that the two diagrams

and

commute for every objects *A*, *B* and *C*.

A *symmetric* monoidal category is a braided monoidal category in which the braiding satisfies

for every objects *A* and *B*.

**Definition** (Closed monoidal category)

A monoidal category is *left closed* when for every object *A*, the functor

has a right adjoint, written

This means that there exists a bijection

which is natural in *B* and *C*.
Equivalently, a monoidal category is left closed when it is equipped with a *left closed structure*, which consists of

- an object ,
- a morphism , called
*left evaluation*,

for every objects *A* and *B*, such that for every morphism there exists a unique morphism making the diagram

commute.

Dually, the monoidal category is *right closed* when the functor admits a right adjoint. The notion of *right closed structure* can be defined similarly.

In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a *closed symmetric monoidal category*.

## Modeling the additives

**Definition** (Product)

A *product* (*X*,π_{1},π_{2}) of two coinitial morphisms and in a category is an object *X* of together with two morphisms and such that there exists a unique morphism making the diagram

commute.

A category has *finite products* when it has products and a terminal object.

**Definition** (Monoid)

A *monoid* (*M*,μ,η) in a monoidal category is an object *M* together with two morphisms

- and

such that the diagrams

and

commute.

**Property**

Categories with products vs monoidal categories.

## Modeling ILL

Introduced in^{[3]}.

**Definition** (Linear-non linear (LNL) adjunction)

A *linear-non linear adjunction* is a symmetric monoidal adjunction between lax monoidal functors

in which the category has finite products.

This section is devoted to defining the concepts necessary to define these adjunctions.

**Definition** (Monoidal functor)

A *lax monoidal functor* (*F*,*f*) between two monoidal categories and consists of

- a functor between the underlying categories,
- a natural transformation
*f*of components , - a morphism

such that the diagrams

and

- and

commute for every objects *A*, *B* and *C* of . The morphisms *f*_{A,B} and *f* are called *coherence maps*.

A lax monoidal functor is *strong* when the coherence maps are invertible and *strict* when they are identities.

**Definition** (Monoidal natural transformation)

Suppose that and are two monoidal categories and

- and

are two monoidal functors between these categories. A *monoidal natural transformation* between these monoidal functors is a natural transformation between the underlying functors such that the diagrams

- and

commute for every objects *A* and *B* of .

**Definition** (Monoidal adjunction)

A *monoidal adjunction* between two monoidal functors

- and

is an adjunction between the underlying functors *F* and *G* such that the unit and the counit

- and

induce monoidal natural transformations between the corresponding monoidal functors.

## Modeling negation

### *-autonomous categories

**Definition** (*-autonomous category)

Suppose that we are given a symmetric monoidal closed category and an object *R* of . For every object *A*, we define a morphism

as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism , we get a morphism , and thus a morphism by precomposing with the symmetry . The morphism is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object *R* is called *dualizing* when the morphism is a bijection for every object *A* of . A symmetric monoidal closed category is **-autonomous* when it admits such a dualizing object.

### Compact closed categories

**Definition** (Dual objects)

A *dual object* structure in a monoidal category is a pair of objects *A* and *B* together with two morphisms

- and

such that the diagrams

and

commute. The object *A* is called a left dual of *B* (and conversely *B* is a right dual of *A*).

**Lemma**

Two left (resp. right) duals of a same object *B* are necessarily isomorphic.

**Definition** (Compact closed category)

A symmetric monoidal category is *compact closed* when every object *A* has a right dual *A*^{ * }. We write

- and

for the corresponding duality morphisms.

**Lemma**

In a compact closed category the left and right duals of an object *A* are isomorphic.

**Property**

A compact closed category is monoidal closed, with closure defined by

*Proof.*
To every morphism , we associate a morphism defined as

and to every morphism , we associate a morphism defined as

It is easy to show that and from which we deduce the required bijection.

**Property**

A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, .

*Remark:* The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify and as well as 1 and .

*Proof.*
The dualizing object *R* is simply *I*^{ * }.

For any *A*, the reverse isomorphism is constructed as follows:

Identity on *A* is taken as the canonical morphism required.