English

Lifting star-autonomous structures

Logic in Computer Science 2023-09-20 v1 Category Theory Logic

Abstract

For a functor QQ from a category CC to the category PosPos of ordered sets and order-preserving functions, we study liftings of various kind of structures from the base category CC to the total(or Grothendieck) category Q\int Q. That lifting a monoidal structure corresponds to giving some lax natural transformation making QQ almost monoidal, might be part of folklore in category theory.We rely on and generalize the tools supporting this correspondence so to provide exact conditions for lifting symmetric monoidal closed and star-autonomous structures.A corollary of these characterizations is that, if QQ factors as a monoidal functor through SLattSLatt, the category of complete lattices and sup-preserving functions, then Q\int Q is always symmetric monoidalclosed. In this case, we also provide a method, based on the double negation nucleus from quantale theory, to turn Q\int Q into a star-autonomous category.The theory developed, originally motivated from the categories PSetP-Set of Schalk and de Paiva, yields a wide generalization of Hyland and Schalk construction of star-autonomous categories by means of orthogonality structures.

Keywords

Cite

@article{arxiv.2309.10422,
  title  = {Lifting star-autonomous structures},
  author = {Luigi Santocanale and Cédric de Lacroix and Gregory Chichery},
  journal= {arXiv preprint arXiv:2309.10422},
  year   = {2023}
}