Date: Wed, 16 Jun 1999 22:24:26 -0700
From: Vaughan Pratt <pratt@cs.stanford.edu>
Subject: categories: Dinaturality in the CCC Poset

The cartesian closed category Pos of posets comes with functors built
using x and ->.  Are there any spurious dinatural transformations between
these functors, in the sense that they cannot be represented in a suitable
simply-typed lambda-calculus?

While the general question is for n-ary functors, the case of unary
functors like Ax(A->A) -> AxAxA should constitute the nub of the problem.

Bob Pare mentioned to me at CT97 in Vancouver that A->A in Pos was "clean"
in this sense, having only the expected dinaturals from A->A to A->A,
namely the Church numerals.  This is in contrast to Set, where Pare and
Roman in a JPAA paper last year (pp. 33-92) gave a litany of spurious
dinaturals for this functor, and also to Chu(Set,2), which likewise
has spurious dinaturals from A-oA to A-oA, albeit of a quite different
character from those of Set.

The only closed monoidal category I'm aware of that contains no spurious
dinaturals in this sense is Girard's *-autonomous category Coh of
coherence spaces, for which Audrey Tan obtained full completeness
for multiplicative linear logic in her 1997 Ph.D. thesis.  That is,
the only dinaturals between functors built using tensor product and -o
are those corresponding to cut-free MLL proofs, the MLL criterion for
"no spurious dinaturals."

What other monoidal closed categories arise in nature that have no
spurious dinaturals?  Are any of them cartesian closed?  In particular
is Pos such?  And how about PER?

Vaughan Pratt