(1) After remembering what the hell the exponential is in presheaf categories, I am pretty confident I have described a monoidal closed structure on Grph that is different from the cartesian closed structure.

(2) But nonetheless there

*is*a cartesian closed structure there: the vertices of A ⇒ B are the graph homomorphisms from A to B, and the edges of A ⇒ B are the graph homomorphisms from

**2**& A to B, where

**2**is the one-arrow graph • → •. And this means A & — is the left adjoint of

*something*, (namely A ⇒ —) and left adjoints preserve colimits, and in particular we must have distributivity

A & (B + C) ⊢ (A & B) + (A & C)

which means that you're no longer in linear logic kansas, but rather in some sort of bunched-logic Oz. But then again, I think I dimly knew this about ICFP paper semantics, too. If you just unwind the definitions of & and + you get distributivity staring you in the face.

Let me just toss in my intended definition of + here, anyhow, just to make that claim falsifiable:

(A, C, f) + (B, D, g) = (A + B, λv.casev ofinlx ⇒ C(x) |inry ⇒ D(y), λv.λm.casev ofinlx ⇒ f x m |inry ⇒ g y m)