poset-valued set

Poset-valued sets


Let PP be a poset and F:RelRelF:Rel\to Rel an endofunctor of Rel. A P FP_F-valued set is a set AA equipped with a function FAPF A\to P.

The category of P FP_F-valued sets inherits a lot of structure from PP: if PP is closed symmetric monoidal, star-autonomous, etc., and FF is well-behaved, then so is the category of P FP_F-valued sets. This provides a general method for constructing models of variants of linear logic.

Category of Poset-Valued Sets

A P FP_F-valued set AA consists of

  1. An underlying set A 0A_0.
  2. A valuation α A:FA 0P\alpha_A : F A_0 \to P

A morphism f:ABf : A \to B of P FP_F-valued sets consists of

  1. An underlying relation f 0:A 0B 0f_0 : A_0 ⇸ B_0
  2. Such that if xF(f 0)yx F(f_0) y then α A(x) Pα B(y)\alpha_A(x) \leq_{P} \alpha_B(y)

This gives a category of P FP_F-valued sets using relational composition. We can further get a double category of P FP_F-valued sets by noticing that the category structure above is the horizontal category of a comma double category, see there for more detail.


If P=3=(012)P=\mathbf{3} = (0\le 1\le 2), with the star-autonomous structure where 11 is both the unit object and the dualizing object, and F(A)=A×AF(A) = A\times A, then the category of P FP_F-valued sets includes the category of coherence spaces as a full subcategory, preserving the closed monoidal structure as well as products and coproducts.


  • Andrea Schalk?, Valeria de Paiva, Poset-valued sets or how to build models for linear logics, In Theoretical Computer Science, Volume 315, Issue 1, 2004, Pages 83-107, DOI.

Last revised on July 30, 2018 at 11:54:07. See the history of this page for a list of all contributions to it.