Seely categories

A Seely category is a model of linear logic.

In more detail, a Seely category \mathcal{C} consists of

a symmetric monoidal closed category (\mathcal{L}, \otimes, 1) ...
... with finite products, denoted by \& and \top
a comonad (!, \epsilon, \delta) on $\mathcal
natural isomorphisms (so-called Seely isomorphisms)

	m_0 : 1 \xrightarrow{\cong}\ !\top

	m_{A, B} :\ !A \otimes !B \xrightarrow{\cong}\ !(A \& B)

such that the diagram

commutes.

As models of Classical Linear Logic

As it stands, a Seely category is a model of intuitionistic Linear Logic. However, the definition can easily be extended to classical linear logic. The key is to ask that the symmetric monoidal closed category (\mathcal{L}, \otimes, 1) is *-autonomous, i.e. that there is an object \bot (the dualizing object) such that the canonical map

	\partial_A : A \to (A \multimap \bot) \multimap \bot

given by currying the evaluation map \textsf{ev}_{A, \bot} : (A \multimap \bot) \otimes A \to \bot is an isomorphism for every object A.

References

An exposition of Seely categories is given in §7.3 of

Melliès, Paul-André. 2009. ‘Categorical Semantics of Linear Logic’. In Panoramas et Synthèses 27: Interactive Models of Computation and Program Behaviour, edited by Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, and Paul-André Melliès. Société Mathématique de France. pdf

@incollection{mellies_categorical_2009,
	title = {Categorical {Semantics} of {Linear} {Logic}},
	isbn = {978-2-85629-273-0},
	url = {http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf},
	booktitle = {Panoramas et synthèses 27: {Interactive} models of computation and program behaviour},
	publisher = {Soci\'{e}t\'{e} Mathématique de France},
	author = {Melliès, Paul-André},
	editor = {Curien, Pierre-Louis and Herbelin, Hugo and Krivine, Jean-Louis and Melli\`{e}s, Paul-Andr\'{e}},
	year = {2009}
}

As evident in the name, the original (slightly faulty) definition of Seely categories is due to Robert Seely.

Seely, R. A. G. 1989. ‘Linear Logic, *-Autonomous Categories and Cofree Coalgebras’. In Categories in Computer Science and Logic, 92:371–82. Contemporary Mathematics. Boulder, Colorado: American Mathematical Society.

@inproceedings{seely_linear_1989,
	address = {Boulder, Colorado},
	series = {Contemporary {Mathematics}},
	title = {Linear {Logic}, $*$-{Autonomous} {Categories} and {Cofree} {Coalgebras}},
	volume = {92},
	booktitle = {Categories in {Computer} {Science} and {Logic}},
	publisher = {American Mathematical Society},
	author = {Seely, R. A. G.},
	year = {1989},
	pages = {371--382}
}

The definition given here is sometimes referred to as a "new Seely category, and is a technical improvement upon Seely's original definition. It is due to Gavin Bierman: it appeared in his 1993 PhD thesis, and then was published in

Bierman, G. M. 1995. ‘What Is a Categorical Model of Intuitionistic Linear Logic?’ In Typed Lambda Calculi and Applications, edited by Mariangiola Dezani-Ciancaglini and Gordon Plotkin, 902:78–93. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0014046.

@inproceedings{bierman_1995,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {What is a categorical model of {Intuitionistic} {Linear} {Logic}?},
	volume = {902},
	isbn = {978-3-540-59048-4 978-3-540-49178-1},
	doi = {10.1007/BFb0014046},
	booktitle = {Typed {Lambda} {Calculi} and {Applications}},
	publisher = {Springer Berlin Heidelberg},
	author = {Bierman, G. M.},
	editor = {Dezani-Ciancaglini, Mariangiola and Plotkin, Gordon},
	year = {1995},
	pages = {78--93}
}

See more discussion in §7.7 of Mellies 2009.