Last week I attended a Category Theory meetup, and as usual, it looks like "standard" notations were chosen to be maximally confusing. And then there's implicit lifting everywhere. 1/n
-
Show this thread
-
A→B, Hom(A,B), Mor(A,B), C(A,B), A⇒B, Bᴬ, [A,B], Nat(A,B): plenty of notations for *sets* (types, categories…) of arrows ((homo)morphisms…), often with overlapping uses. Why not a single universal notation, an arrow with optionally the category under it to disambiguate?
1 reply 0 retweets 1 likeShow this thread -
It's often important to distinguish an "internal" A⇒B in a category from an "external" A→B in its meta-category… that itself somehow has all arrows internal. Indeed many theorems actually relate arrows at many different levels, which the baroque notations maximally obfuscate.
1 reply 0 retweets 0 likesShow this thread -
Category theory notation starts and stops magic implicit lifting at random, forcing everyone to have complex type and kind inference—that even top specialists sometimes admit to get wrong. Instead of either magic or painful explicit lifting, use quasiquotation and escape!
1 reply 0 retweets 1 likeShow this thread -
In computer science, eval and apply mean very distinct things, but of course, category theorists call "eval" what everyone else calls "apply" (yet correctly call "partial application" by its name). Category theorists? More like Category Terrorists!
1 reply 0 retweets 0 likesShow this thread -
Internal (first-class) functions vs their semantics as external functions; relationship between theory and meta-theory; quotation and (lack of proper) quasiquotation; eval and apply... Category Theorists are just reinventing Lisp, badly, except with ((heavily) dependent) types.
1 reply 0 retweets 2 likesShow this thread -
Category theorists should seriously learn some Lisp. And Conversely, lispers should learn themselves some dependent types.
1 reply 0 retweets 1 likeShow this thread -
Introductions to CT make you believe it's all about preserving the compositional structure of nodes and arrows, but actually, it's about preserving the compositional structure of arbitrarily complex diagrams over increasingly many nested levels of nodes and arrows.
1 reply 0 retweets 0 likesShow this thread -
Category Theory is complex enough that you need all the help you can to understand it, but Category Terrorists invent notation that is maximally confusing with what Mathematicians use, what Computer Scientists use, what Logicians use, and what other Category Terrorists use.
1 reply 1 retweet 3 likesShow this thread -
Some day, I'll understand enough Category Theory to do my own variant with blackjack and hookers—and some coherent notation. And either all the arrows will go from right to left, or function application will be postfix by default.
1 reply 0 retweets 2 likesShow this thread
The most elementary result of Category Theory, Yoneda's Lemma, requires three levels of arrows, relating internal arrows to external ones that preserve two levels of arrows. Nothing is interesting below three levels: 1. Morphisms, 2. Functors, 3. Natural Transformations.
-
-
There seems to be no convention for diagrams over multiple levels of arrows. Wikipedia's page for the Yoneda Lemma has a semi-nice one with one square inside another, but only position relates two levels, and for more complex diagrams, you'll need at least a third dimension.
0 replies 0 retweets 0 likesShow this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!