Categorical semantics

Revision as of 18:14, 23 March 2009

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

See ^[1]for a more detailed introduction to category theory.

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

Definition (Monoidal category)

A monoidal category $(\mathcal{C},\otimes,I)$ is a category $\mathcal{C}$ equipped with

a functor $\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}$ called tensor product,
an object $I$ called unit object,
three natural isomorphisms of components

$\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C) \qquad \lambda_A:I\otimes A\to A \qquad \rho_A:A\otimes I\to A$

called respectively associator, left unitor and right unitor,

such that

commutes,

commute.

Definition (Braided, symmetric monoidal category)

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

$\gamma_{A,B}:A\otimes B\to B\otimes A$

called braiding, such that the two diagrams

UNIQ41bde98e566e91d2-math-0000000E-QINU

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

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

$\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B$

for every objects $A$ and $B$ .

@@ Line 3: / Line 3: @@
 See <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag,year=1971,volume=5,series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory.
-== Modeling [IMLL] ==
+== Modeling [[IMLL]] ==
-A model of [IMLL] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.
+A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.
 {{Definition|title=Monoidal category|
@@ Line 39: / Line 39: @@
 for every objects <math>A</math> and <math>B</math>.
 }}
 == References ==
 <references />