Multi-classed Software Engineer/Constructive Mathematician. Sometimes plays video games sort of fast. Puts topoi in your computer. https://teapawt.net/t.co/iFlKRVeGpN
Joined March 2019
- Tweets5.9K
- Following21
- Followers715
- Likes555
So, I was thinking. When we write ⊢A→B ∧ ⊢A ⟹ ⊢B in inference rules. What is the pattern A→B as a mathematical object? 1/8
Now our conditions become g∘f≤id and id≤f∘g (hint: id is minimal). That is f and g form a Galois connection (equivalently ∀a x, x≤f(a) ⟺ g(x)≤a). I think it generalises: in a subtyping situation, you don't typically have x=f(a) only x≤f(a). Exactly what shows up! 7/8
This is important dl.acm.org/doi/10.1145/38286… . For instance, when you have a linear Int# in Haskell, it's the same as having an unrestricted Int#. You want the type system to understand that, that's what the authors call mode crossing. 1/2
What I'm suggesting is that we can, and probably should, take this as the *definition* of multicategories (it's a tad more general: ordinary multicategories correspond to the case where contexts are a PROP generated by the pures).
Something I realised while working on sheaves (because it turns out to be relevant) is that the multicategorical definition of coproduct is stronger than the categorical one. Because in the multi case, the branches have access to the context. In the cat case they don't. 1/3
Hom(A+B, X) ≃ Hom(A,X)×Hom(B,X)
vs
Hom((Γ,A+B), X) ≃ Hom((Γ,A), X)×Hom((Γ,B), X)
(assuming symmetry for simplicity) 2/3
In June, Ocaml 5.5 was released ocaml.org/changelog/2026-06-… , whose headline change is module-dependent functions (aka modular explicits)
The Ocaml mailing list is no longer online, but I found in my emails me from May 2012, trying (and failing) to garner support for this feature 1/2
At the time it didn't have a name. There was no paper. And it got basically no interest at all.
I'm really happy now. I've been looking forward to this moment for almost 15 years.
Someone on the butterfly network found this archive. So here is the said email inbox.ci.dev/caml-list/CAMoP… 3/2
I noticed something the other day. If you have a monoidal category, and a subset P of objects, then arrows from arbitrary objects to objects of P form a multicategory. We'll say that this is a category of context and P are pure objects. 1/8
From a PLT perspective, this is a friendlier re-analysis of the contextuals CCC teapawt.net/aspiwack/status/204213… . See also Shulman's multicategorical logic tutorial mikeshulman.github.io/catlog… . 7/8