Two further thoughts:

(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.case v of inl x ⇒ C(x) | inr y ⇒ D(y),
λv.λm.case v of inl x ⇒ f x m | inr y ⇒ g y m)
```
Tags:
• #### (no subject)

Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

• #### (no subject)

Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

• #### (no subject)

I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic