Oh no! At first I thought this paper was just bing silly/clever with `⟅⟆ : Bag` (it looks like a bag 💰 haha), but then I realised this is actually a thing! Unicode calls them 'bag delimiters'… 😱
Conversation
Replying to
And so followed my first hunt for the history of a character's introduction into unicode: unicode.org/L2/L2003/03410 - no idea what the history is of these characters in mathematics though... 🤔
4
11
Apparently they come from Squiggol!
Quote Tweet
Replying to @Teggy and @brendanzab
Indeed I do. They were whiteboard notation in the Squiggol community in late 80s, early 90s. @asajeffrey and I put them in the St Mary's Road symbol font. I guess Unicode picked them up from there.
1
3
Also known as the "Bird–Meertens formalism":
> Facetiously it is also referred to as Squiggol, as a nod to ALGOL, which was also in the remit of WG 2.1, and because of the "squiggly" symbols it uses.
⟅😂⟆
1
1
Quote Tweet
Replying to @samthecoy and @FakeUnicode
This was the paper that led to the goose chase for squiggolly bag symbols: S-C. Mu, H-S. Ko, and P. Jansson. "Algebra of programming in Agda: dependent types for relational program derivation" iis.sinica.edu.tw/~scm/2009/alge
1
This was the paper that led to the goose chase for squiggolly bag symbols: S-C. Mu, H-S. Ko, and P. Jansson. "Algebra of programming in Agda: dependent types for relational program derivation" iis.sinica.edu.tw/~scm/2009/alge
1
1