Jason (jcreed) wrote,

Had a thought in the shower this morning about the fact that the free commutative monoid monad isn't cartesian — something I had got really bummed about since finding it out yesterday. I think I understand better now that to use it for the context-structure monad would be like having a sequent where things were so deeply commutative that you couldn't even tell one hypothesis of proposition A from another: as if you didn't even have labels or variable names or anything. Now while this would still work just as well for raw provability in place of real proof theory (parallel to the vanishing of all concerns about the monad being cartesian (i.e. preserving pullbacks and having natural transformations whose naturality diagrams are pullbacks) if we were working with just posets and not categories) of course our notion of proof would be fucked up if different hypotheses were totally indistinguishable up to permutation, i.e. if variables didn't have names.

Instead, we give them names, and understand that there is an exchange property or rule, for which we might have to do some real work like swapping around deBruijn indices when we perform it. Once again my problems are due to the forgetting the Fundamental Lesson of Weak n-Category Theory, to wit,
don't think things need to be identical when they merely need to be isomorphic
Tags: math, work

  • (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


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded