Physicist, programmer (Haskell, C++), mathematician, category theorist. Author of Category Theory for Programmers and The Dao of Functional Programming
Public Key
npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Profile Code
nprofile1qqs2vz5gxaxcu88sjtr74ymx92ncf7enk0n4hemj2qtsxtnf984ut4gpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dss2u4xn
Show more details
Published at
2026-07-11T15:18:06Z Event JSON
{
"id": "4971a6547ff69bf43ea71acab76627aa53edb18b71e38f87c6e0f23e37ad2270" ,
"pubkey": "a60a88374d8e1cf092c7ea93662aa784fb33b3e75be7725017032e6929ebc5d5" ,
"created_at": 1783783086 ,
"kind": 0 ,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/BartoszMilewski",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "{\"name\":\"Bartosz Milewski\",\"about\":\"Physicist, programmer (Haskell, C++), mathematician, category theorist. Author of Category Theory for Programmers and The Dao of Functional Programming\",\"picture\":\"https://media.mathstodon.xyz/accounts/avatars/108/205/154/379/845/901/original/862ec704f5fa1247.jpg\",\"nip05\":\"[email protected] \",\"fields\":[[\"blog\",\"https://bartoszmilewski.com/\"],[\"github\",\"https://github.com/BartoszMilewski\"],[\"book\",\"https://github.com/BartoszMilewski/DaoFP/blob/master/DaoFP.pdf\"]]}" ,
"sig": "be805c9ad4a58ee916e9e563c43982b4a6b23686df22c99b79b01b90c162ffb85c514f0370cd3618be49bb76ba4ff9be8532b951da6647d5a1b7828896e18ce0"
}
Last Notes npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I just realized that Chekhov's Gun is an example of linear logic. It's a premise that has to be consumed at some point in the plot. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski The paradox of the stone: "Could God create a stone so heavy that even he could not lift it?" was solved by Grothendieck by introducing an infinite tower of gods. The God of the n'th universe can only create stones that he can lift. But the God from the n+1 universe can create an unliftable stone for the God from the n'th universe, and so on. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Democracy is like health: You don't appreciate it until you lose it. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc @nprofile…gu9p @nprofile…ck2y npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…ck2y @nprofile…g0zc @nprofile…gu9p npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…5pn7 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…5pn7 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski We can take a derivative of a container with respect to an isolated object \(p_0 \colon P s\). The shapes in the derivative are pairs of objects \( (s \colon S, p_0 \colon P s ) \) and the positions are functors to \(P s \textbackslash p_0 \) (the category \(P s\) with the (isolated) object \(p_0\) removed). npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Now replace sets with categories. A categorical container is a category of shapes \(S\) and a (pseudo-) functor \(P \colon S \to \mathbf{Cat}\). It's the same functor that appears in the Grothendieck construction. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I have found an interesting link between containers and the Grothendieck construction. Here's a sketch. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Geoffrey Hinton came up with the same conclusion. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I see parallels between the current situation in Iran and the Solidarity movement in Poland in 1980. Back then I went on a business trip to the Soviet Union. A Russian friend told me that we were lucky their troops were busy in Afghanistan. They are now busy in Ukraine, so I have high hopes for Iran. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…4hp5 @nprofile…hvu9 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…gj0l npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc She just did "Best Actress in a Drama Series" at the Critics Choice Awards! npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…gj0l npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…g0zc npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I have a feeling that homotopy type theory might be a better foundation for music theory. For instance, two pitches an octave apart are often described as equal, but it's a non-trivial equality. One might say that there is a "path" between them. Different chord inversions are also "equal" in this sense. A thirteenth chord can be identified with an added sixth, and so on. Then there are chords that are missing the third or the fifth. Such chords can be idenitified using more than one path, so you may have higher homotopies. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…hzey npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…pjrp npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…hzey npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…hzey npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…3tgm @nprofile…kkj3 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…v64a npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…kkj3 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Math is next on the chopping block. The AI was able to master chess and go because it was given the rules of the game and an oracle to evaluate the result of each game. We now have several formalizations of math and theorem checkers to evaluate the results. So it's just a matter of time. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski We assume that the brightness of all supernovae of Type Ia is more or less the same. We can use them as 'standard candles' to measure the distance to remote galaxies. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…drul npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…sju8 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…6k70 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…drul npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…6k70 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…atf6 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski How sure are we that there were never any intelligent dinosaurs? How much of fossil evidence would survive 66 million years? Would pyramids survive this long? npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Turns out, last week there was a massive rename of the two fields in Iso involving 281 files. Hence my problem. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Apparently I'm supposed to use v.09 of the library, but I'm unable to clone it npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski The latest cubical Agda repository has this definition: npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…y5fr npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski \[ \mu Y \ldotp 1 + X \times Y \] npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…c0p4 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…65we npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I hate this notation: npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…rwld npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski The future of LLM-assisted mathematics: npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski You can catch more dark matter with honey than with vinegar. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I like the attention to detail in Pluribus. I think it's the first time that an intravenous injection was shown correctly on camera (usually they just stab the patient with the needle perpendicular to the surface). We also learned that Zosia was from Gdańsk --and she pronounced it correctly (Karolina Wydra is a Polish-American actress). npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I'm wondering if there is a maximal category, such that every small category is a subcategory of. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski A typical dialog: npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua @nprofile…v6hh npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…tcm7 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski A physicist's brain is trained on the Standard Model data. No wonder we are constantly looking for more gauge groups and Higgs fields. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski The US is experiencing a Tourette's syndrome with Donald Trump being its mouthpiece. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…9s72 @nprofile…stct npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…stct npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski If you want to learn how not to write dialogs in a SciFi show, watch Invasion. All characters are eqully brain dead, and their only purpose is to make idiotic moves and talk about their feelings ad nauseam with a lot of dead air in between. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua What's fascinating about burds is that they have to be very thrifty with their brains, or they wouldn't be able to lift them into the air. And their brains have to deal with 3-d navigation and superior vision. Compared to birds, human brains are extremely wasteful. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Instead of terraforming Mars, humanity opted for terradeforming Earth npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua @nprofile…drul @nprofile…stct I'm imagining a taffy machine running for billions of years, with an emerging Taffian civilization discovering Taffian physics, when suddenly the movement is reversed. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua @nprofile…stct I wonder if it could be undone. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…stct Intimidation works! npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…03p3 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Suppose you were outfitting a school in the middle of Africa. What would be the best way to provide it with internet access? Is there an alternative to StarLink? npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…emex npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Type theory and category theory are the product of highly refined abstractions. Since every level of abstraction strips a layer of intuition, the final product is sometimes called abstract nonsense. The only way to navigate such vast halls of abstraction is to keep in mind where those abstractions come from, or how they can be modeled in more familiar surroundings, be it computer programs, logic, or set theory. When studying an elephant, it makes sense to occasionally focus on its trunk, legs, or ears, npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski I think we should immediately start ostacizing people on social media who publish AI slop without proper attribution. It's not funny! npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn In my paper on nerual lenses I introduced a triple Tambara module. (I had to shrink the notation, so each bolded category corresponst to a product, eg \( \mathbf C = C^{op}\times C\), etc.) npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski A trace-monoidal category is equipped with a trace: npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…cvnq npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…cvnq npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Some of us remember the times when plastics were cool. PVC floors, formica countertops, acrylic furniture, melamine dinnerware, polyester clothes. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…0775 npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…0775 I guess we are saying the same thing, with a different emphasis. I would reword your result as "given an actegory one can always construct a locally graded category that is equivalent to the Para construction." npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski After I finished The Bear, Disney's Artificial Idiocy suggested I watch "L'Ours": The stories of an orphaned bear cub, a big lonely bear and two hunters in the forest. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…0775 @nprofile…p3nn I think I misunderstood the para/graded equivalence. My intuition was that Para on top of an actegory, with parameterized hom sets \(a \bullet m\to b\) is equivalent to a locally graded category with hom-sets graded by M (a category enriched over [M, Set]). But you seem to show that a graded category is equivalent to the actegory itself, not the Para. Am I wrong? npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…0775 @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…0775 : Wouldn't a co-para construction correspond to a locally graded category over co-presheaves? I haven't done the calculation, but it seems intuitive. npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn Except in your blog? npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…p3nn npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…stct npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…stct npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Without looking at the sky, the stars, the Moon, or the Sun, you just count the steps npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski Clocks are the instruments of dead reckoning in time npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski @nprofile…8eua @nprofile…y0ah npub15c9gsd6d3cw0pyk8a2fkv248snan8vl8t0nhy5qhqvhxj20tch2swwczp5 Bartosz Milewski So far enjoying "The Last Frontier". Less gore, more brain.
