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