It gives a recipe for constructing models of linear logic that have specified properties, by starting from a poset that has the required properties and constructing a category based on that. There is something rather mystifying about the construction as it stands, so I wondered whether there’s some way of thinking about it that sheds more light on it. I think there is, and I may as well record it here in case anyone is interested. The ingredients of the construction are: a poset P that has some additional (monoidal, monoidal closed, star-autonomous) structure, and a lax monoidal functor F: Rel → Rel. These ingredients are used to construct a (monoidal, etc.) category PFSet.
Now, there is a standard construction that builds from any category C a category Rel(C) that can be described concretely as follows: an object of Rel(C) is a set S together with a function fS: S → |C|, and a morphism r: S → T consists of a relation S → T together with, for every (x,y) ∈ r, a set of C-morphisms from fS(x) to fT(y). Abstractly, Rel(C) is the free sup-lattice-enriched category with small biproducts generated by C, which can be constructed by freely changing the base of enrichment and then freely adding the biproducts.
For any C there is an obvious forgetful functor U: Rel(C) → Rel. My basic observation is that the category PFSet is precisely the pullback of F: Rel → Rel and U: Rel(P) → Rel. (The assumption that P is a poset rather than an arbitrary category does not seem to have any effect beyond simplifying the concrete description of the result.)
The interesting part is the monoidal structure. For the sake of simplicity, just suppose that C is monoidal; we want to see how a monoidal structure is induced on PFSet. It’s easy to see that Rel(C) inherits, and U strictly preserves, any monoidal structure possessed by C. On the other hand, F is only lax monoidal (or equivalently oplax monoidal, since Rel is self-dual), so that doesn’t immediately help. At this point, perhaps it makes things easier to abstract away from the details for a moment. We have a pullback like this:
where the three categories we started with (C, D and E) are all monoidal, U is strict monoidal, and F is oplax monoidal. It turns out that if U is a fibration then there is a natural way to define a monoidal structure on B. (I’m not sure whether this has been observed before [update: it has – see Richard’s comment below], but it’s quite easy.) Furthermore, U doesn’t actually need to be a fibration: the only maps that need to have cartesian liftings are the structural maps F(A⊗B) → FA⊗FB and FI → I that give the oplax monoidal structure on F.
Coming back to our concrete U: Rel(C) → Rel, there are two simple extreme cases: on the one hand, a relation that is the graph of a function always has a cartesian lifting; on the other, if C has (set-indexed) products then every relation has one (so in this case U really is a fibration). The former case is the one that’s addressed in the paper – it’s assumed that the structural maps are always graphs of functions – but it’s clear from what I’ve just said that this can be generalised. In the former case our general construction does seem to give the same result as the concrete description in the paper.
The same idea can certainly be extended to monoidal closed structure: in this case we need F to be lax monoidal as well as oplax monoidal, which is a triviality in the concrete case in question. I haven’t thought about star-autonomous structure, but I would be surprised if that didn’t work too.