*-Autonomous category

Let be a symmetric closed monoidal category (cf. also Category). A functor is a duality functor if there exists an isomorphism , natural in and , such that for all objects the following diagram commutes:

where in the bottom arrow .

A category is -autonomous if it is a symmetric monoidal closed category with a given duality functor.

It so happens that -autonomous categories have real-life applications: they are models of (at least the finite part of) linear logic [a2] and have uses in modelling processes.

An example of a -autonomous category is the category of sets and relations; duality is given by . In fact, .

From a given symmetric monoidal closed category and an object in it (that serves as a dualizing object) one can construct a -autonomous category (the so-called Chu construction, [a3]). It can be viewed as a kind of generalized topology.

References

[a1]	M. Barr, "-Autonomous categories" , Lecture Notes in Mathematics , 752 , Springer (1979)
[a2]	M. Barr, C. Wells, "Category theory for computing science" , Publ. CRM (1990)
[a3]	P.-H. Chu, "Constructing -autonomous categories" M. Barr (ed.) , -Autonomous categories , Lecture Notes in Mathematics , 752 , Springer (1979) pp. Appendix