higher categories
October 14, 2019 6:09 AM   Subscribe

With Category Theory, Mathematics Escapes From Equality - "Two monumental works have led many mathematicians to avoid the equal sign. Their goal: Rebuild the foundations of the discipline upon the looser relationship of 'equivalence'. The process has not always gone smoothly."

John Baez adds context![1]
One thing that's happening now, at least: @emilyriehl and Dominic Verity are developing a "synthetic" approach to (∞,1)-categories, which characterizes them axiomatically instead of "building" them as Boardmann-Vogt, Joyal, Lurie and others did.

There are many different ways to build (∞,1)-categories from sets. For example, in 2006 Julie Bergner showed that 4 different ways are equivalent: A survey of (∞,1)-categories

The "synthetic" approach isolates what these different approaches have in common.

"Homotopy type theory" is another synthetic approach to higher categories, different but in the same spirit.[2]

It may take a decade or two for all this to settle down, but ultimately good textbooks will make (∞,1)-categories much easier to learn and use!

So far they are mainly useful in topology, algebraic and differential geometry, and the kind of physics that exploits these subjects. They are also infiltrating computer science. As easier textbooks get written, people will dream up more new applications.

Will I ever use them myself? I don't know.

I switched to "applied category theory" because I decided there were lots of great things to do with plain old 1- and 2-categories in engineering, chemistry, computer science... and some day, I hope, biology.[3]

But someday, when we've really figured out what 1- and 2-categories are good for in the sciences and engineering, we may see good reasons to use (∞,1)-categories.

Meanwhile the pure mathematicians may have moved on to (∞,n)-categories!

Reading material:
  • Lurie's "Higher Topos Theory"

  • Lurie's "Higher Algebra"

  • Riehl and Verity's "∞-Categories for the Working Mathematician." This is really about (∞,1)-categories.

  • Also try this video of a talk by @emilyriehl. [jump to 34m56s for the Curry-Howard-Voevodsky correspondence :]
  • also btw...
    Category Theory and Context: An Interview with Emily Riehl - "Emily Riehl is an incredibly accomplished early-career mathematician, working at the interface of category theory and homotopy theory. She is also a stunning number of other things, including a creative interdisciplinary scholar, working musician, and high-level athlete... on the US women's national Australian Rules football team."[4,5,6]

    The Women Taking Math To The Next Dimension - "Rebecca Goldin, Emily Riehl, and Eugenia Cheng share their favorite puzzles, explain why math is like a dragon, and give tips for young women entering the field."
    posted by kliuless (40 comments total) 38 users marked this as a favorite
     
    Dr. Eugenia Cheng talking about applications of category theory to real life, including intersectionality.
    posted by acb at 6:22 AM on October 14, 2019 [2 favorites]


    YOU CAN'T MAKE ME LEARN NO NEW MATH

    *realizes no one is forcing me to learn anything*

    Huh. Cool.
    posted by sugar and confetti at 7:39 AM on October 14, 2019 [5 favorites]


    How math works.
    posted by Navelgazer at 7:40 AM on October 14, 2019 [4 favorites]


    But... can you trisect an angle with Category Theory?
    posted by sammyo at 7:48 AM on October 14, 2019 [7 favorites]


    Navelgazer: Mathematicians are weird.
    posted by aleph at 7:55 AM on October 14, 2019 [3 favorites]


    This looks an awful lot like when I learned that the "multiplication" cross product (×) sign and the dot product signs (·) meant different things, but my 6th grade teacher told us they meant the same thing and were always interchangeable, and I got in trouble because i made a stink about it in class.

    Of course, being in a private Catholic school, I'm pretty sure my 6th grade teacher didn't even have a bachelor's degree, and never in her life took a class where vectors were involved, and was adamant that I was wrong. (This is the same teacher who petitioned the principal to hold me back in 6th grade not because I was failing any classes, but because I refused to do my homework. I was promoted to 7th grade only after signing a pledge that I would do all my homework in the future. Reader, I did not fulfill my pledge.)

    They're interchangeable in 6th grade arithmetic, yes, but clearly they have COMPLETELY different results and meanings in other contexts.

    The equals sign is never going away, but the notion of equivalence in categories is going to continue to expand the subtleties of math.

    But can the press NOT fire out salvos to the public saying the equals sign is going to go away, or that it doesn't mean anything anymore? Chalk this up as another example of journalistic malpractice in the headlines only to walk it back a bit in the article itself, and if I may be forgiven for injecting politics here, this is how we ended up with fucking Donald Trump: provocative "teaser" headlines and buried subtleties in a world where the headline is NOT taken as a teaser to a deeper analysis, but for a large enough set of readers to elect Presidents is the whole, core takeaway.
    posted by tclark at 8:00 AM on October 14, 2019 [19 favorites]


    tclark: Somehow I see you at the edge of the Ocean shouting at the advancing waves. (Keep doing it please)
    posted by aleph at 8:05 AM on October 14, 2019 [3 favorites]


    I have to repeat the response my mathematician wife sent me when I asked about this:
    "Equals means `is exactly the same thing as'. But there are comparisons that are like equal that are good enough or better in certain contexts. Example: MeUndies makes lots of copies of the same pair of underwear every month. You don’t care which pair you get in the mail because they’re basically the same (equivalent). But a month later, you definitely care which pair you put on in the morning (equals)."
    posted by Navelgazer at 8:52 AM on October 14, 2019 [21 favorites]


    As a software dev I notice the idea of 'type' in compiler theory to be closely related or influenced by categories via HoTT (Homotopy type theory) and can see that it could be really helpful, but the duck typing daemon hops on my shoulder and whispers, "it all compiles down to the same machine instructions".

    I wonder if this is equivalent to the underwear example, and could that be proven by some Lurie Lemma?
    posted by sammyo at 9:13 AM on October 14, 2019 [1 favorite]


    soooooo am I going to have to reread my algebra, topology, and algebraic topology textbooks for this? I am not opposed to this, like, at all, just...yeah.
    posted by schadenfrau at 10:04 AM on October 14, 2019


    Yeah I realized recently if I'm going to further my commitment to strong static types I'm going to have to get into category theory. Thanks for the roundup!
    posted by PMdixon at 11:37 AM on October 14, 2019


    Hm, interesting. I've been trying to teach myself a little bit of category theory on a hunch that it will be a really powerful new way of thinking about both data analysis and modeling for my research. The impression I've come away with so far is that the main shift in thinking is not necessarily from equality to equivalence (though that does seem important) but from intrinsic properties to extrinsic relations. It seems likely the project of category theory is in some sense to reformulate mathematics in a way that is agnostic to the notion of what a mathematical object is and instead cares only about what it does. Which then implies that equivalence is the more important concept. To me this seems very appealing, as it fits how I think about not only mathematics but ontology more broadly. But I'm still very unsophisticated in my understanding of the subject, and my perspective here may not be the same as the mathematicians who understand it better than I do.
    posted by biogeo at 11:38 AM on October 14, 2019 [2 favorites]


    Can anyone in the know explain to me what things like this or homotopy type theory offer in terms of providing a more workable foundation for mathematics than ZFC? I understand the conceptual value of representing mathematical objects intensionally*, and then (if I understand this right from a high level) the value of treating categories as topological spaces for the sake of defining a notion of equivalence paths that you can then carry propositions across, but I remember this comment saying that HoTT avoids the problem of having to prove e.g. the equivalence of non-negative integers with the naturals, but wouldn't an intensional type theory still require that you construct a path between the two representations? Is it just that the constructive underpinnings make that easier somehow?

    Bonus question: what does the "homotopy" part of HoTT offer or enable beyond something like, say, the calculus of constructions?
    posted by invitapriore at 11:48 AM on October 14, 2019


    Category theory has never really clicked for me, but reading that article I feel like I might finally be experiencing at least the ghost of a departure toward a qualitative understanding.
    posted by jamjam at 1:03 PM on October 14, 2019


    Wrapping my head around the category-theoretic representation of a monoid* was the crucial step for me in getting a basic feel for just what level of abstraction it is that categories operate in. Before that, it was really hard to step outside of the set-with-functions model.

    If I remember right, the category has only a single object, which isn't really anything beyond being the domain and codomain of all the morphisms involved. The morphisms map to the elements of the set X if you were thinking of the monoid in terms of the group-theoretic definition (X, 0, +), so for example if X is the naturals, you have a single-object category where 1 is a morphism from the object to itself, and the composition of the 1 morphism twice is equivalent to the 2 morphism, etc. It's pretty cool.
    posted by invitapriore at 1:27 PM on October 14, 2019


    Oh, wait, where have I heard the name Eugenia Cheng before? Ah, yeah previously: How does pure mathematics apply to our daily lives?

    Same presentation I think that acb linked, but given at The Royal Institution.
    posted by zengargoyle at 1:29 PM on October 14, 2019 [1 favorite]


    I've been trying to teach myself a little bit of category theory on a hunch that it will be a really powerful new way of thinking about both data analysis and modeling for my research

    Was this precipitated by UMAP?
    posted by en forme de poire at 1:32 PM on October 14, 2019


    In a strange way, category theory seems to have been foreshadowed by Dedekind cuts, in which numbers, which were formerly conceived as terminally basic, are replaced by sets with vast and recursive internal structures, a lot like the way equality is replaced by "infinite towers of equivalence" in category theory.
    posted by jamjam at 2:05 PM on October 14, 2019 [2 favorites]


    No, actually, that one just makes me think I should learn more differential geometry. I hadn't really considered it much though; do you think category theory is an important foundation for UMAP?
    posted by biogeo at 2:07 PM on October 14, 2019


    The paper does recommend a background in category theory and starts busting out functors and simplicial sets right off the bat -- though I've also heard the theory is not actually that relevant to the computations UMAP actually ends up doing.
    posted by en forme de poire at 2:28 PM on October 14, 2019 [1 favorite]


    Another useful resource for learning about category theory is Bartosz Milewski's free ebook Category Theory For Programmers. (There's an unofficial LaTeX/PDF version here.)
    posted by acb at 3:57 PM on October 14, 2019 [2 favorites]


    Thanks for that link! I'd seen some of Milewski's talks on YouTube, but their pace didn't quite match what I needed or something. I've been working through Category Theory for Scientists by David I. Spivak, which has been pretty good for me so far.
    posted by biogeo at 4:22 PM on October 14, 2019 [2 favorites]


    You fellers just move along, we don't want no monads 'round these parts. (spits tobacco into urn)
    posted by RobotVoodooPower at 5:31 PM on October 14, 2019 [3 favorites]


    how do I learn enough about math to begin to be able to approach this subject? I kinda missed the boat on enjoying math in high school and college for various reasons but I’ve here and there wished I could understand stuff like this.
    posted by Gymnopedist at 5:34 PM on October 14, 2019


    I enjoyed Eugenia Cheng's How to bake Pi, which requires almost no math knowledge. It's not terribly deep, but there are some insights in there.
    posted by Monday, stony Monday at 5:49 PM on October 14, 2019


    Lawvere's "Conceptual Mathematics" is about a good a basic introduction to category theory for people without some reasonable amount of mathematical experience as you might find, although it's kind of an odd take compared to mainstream category theory. Still, it manages to do quite a bit of interesting stuff without dragging in a lot of knowledge of algebra and topology.
    posted by Death and Gravity at 6:00 PM on October 14, 2019


    My lay sense is that category theory is pretty hard to motivate without having some grasp on the things it's attempting to abstract over (groups in particular it seems to me), but honestly, I don't know that much about it, so I'd defer to Death and Gravity's recommendation.
    posted by invitapriore at 6:26 PM on October 14, 2019


    The TLDR for the univalence axiom (part of HoTT) has stuck with me for quite a while: equivalence is equivalent to equality
    posted by hambone at 6:30 PM on October 14, 2019 [1 favorite]


    I had Emily Riehl as a TA for a math class in college, maybe more than one. I can't remember even which classes but I remember her being excellent at teaching math and just a very open, friendly, generous person. I'm glad her career is going so phenomenally well.
    posted by smelendez at 6:37 PM on October 14, 2019 [1 favorite]


    but the duck typing daemon hops on my shoulder and whispers, "it all compiles down to the same machine instructions".

    You don't write the machine instructions, do you? So who cares how it's implemented?
    posted by kenko at 6:42 PM on October 14, 2019 [1 favorite]


    but the duck typing daemon hops on my shoulder and whispers, "it all compiles down to the same machine instructions".
    You don't write the machine instructions, do you? So who cares how it's implemented?

    This seems pretty needlessly snarky, and contentless besides. I would challenge the quoted notion by saying that the benefit you get from rigorous reasoning about types at the language level is that, whatever their ultimate translation to machine instructions is, you have much stronger guarantees that the translation in question maintains the invariants you specify in the higher-level language.
    posted by invitapriore at 6:59 PM on October 14, 2019


    I've seen Seven Sketches in Compositionality: An Invitation to Applied Category Theory, by Brendan Fong and David I. Spivak, recommended as a good introduction to CT, also for readers who don't have a PhD in Math.

    arXiv.org link
    PDF (at arXiv.org)
    Lecture Series (poor audio quality, unfortunately)

    From the introduction:
    The purpose of this book is to offer a self-contained tour of applied category theory. It is an invitation to discover advanced topics in category theory through concrete real-world examples. Rather than try to give a comprehensive treatment of these topics—which include adjoint functors, enriched categories, proarrow equipments, toposes, and much more—we merely provide a taste of each. We want to give readers some insight into how it feels to work with these structures as well as some ideas about how they might show up in practice.

    The audience for this book is quite diverse: anyone who finds the above description intriguing. This could include a motivated high school student who hasn’t seen calculus yet but has loved reading a weird book on mathematical logic they found at the library. Or a machine-learning researcher who wants to understand what vector spaces, design theory, and dynamical systems could possibly have in common. Or a pure mathematician who wants to imagine what sorts of applications their work might have. Or a recently-retired programmer who’s always had an eerie feeling that category theory is what they’ve been looking for to tie it all together, but who’s found the usual books on the subject impenetrable.
    Disclaimer: I have zero math chops, haven't finished Chapter 1 yet, and feel like I'll probably need to read Chapter 1 several times before it (hopefully) sinks in.
    posted by syzygy at 7:41 PM on October 14, 2019 [4 favorites]


    I cannot comment on Category Theory as mathematics per se (for astrophysicists, maths is merely another screwdriver to use as a hammer) but it looks like a fascinating area of anthropological study. So many religious tropes...
    posted by fallingbadgers at 8:39 PM on October 14, 2019


    > I would challenge the quoted notion by saying that the benefit you get from rigorous reasoning about types at the language level is that, whatever their ultimate translation to machine instructions is, you have much stronger guarantees that the translation in question maintains the invariants you specify in the higher-level language.

    Yes. The other issue is that anything beyond a few dozen or, certainly, a few thousand or million machine language instructions is getting into a realm of complexity where

    #1 It is pretty hard to keep a handle on what is going on without some higher-level logical constructs to back things up

    #2 Those constructs help you build things that you could never possibly have conceived or dreamed of using only the basic lower-level building blocks

    #3 The more powerful your logical constructs, the more powerful the systems you can imagine, understand, comprehend, build, and have confidence in

    A couple of examples just to give an overall sense of what I'm talking about:

    - It is theoretically possible to build a baby just by taking raw atoms and molecules and adding one to another to another very, very carefully until you end up with a complete baby. After all, babies are made of nothing but raw atoms and molecules!

    But in fact no one in their right mind would make a baby or even a far simpler thing--say a piece of granite--that way. Instead we leverage a whole tried and true--and very deep--stack of tools whose ultimate effect is indeed to arrange a whole lot of atoms into a working baby, piece of granite, stool, or whatever else we are trying to make.

    - It is theoretically possible for someone to sit down and just hard code in machine language the functional equivalent of, say, a deep learning neural network that does a pretty reasonable job of translating one language to another.

    When you get finished with a few hundred hours of training the network, all you come out of that with is a bunch of bits, right? So a very, very smart person could have just started typing out those bits and skipped the whole apparatus of deep learning, training sets, etc etc etc.

    Just jump right to the end result.

    In fact--somewhat contradicting what I just said--I don't really believe creating a baby or the results of a complex deep learning neural network training can (even theoretically) be made from scratch using just basic building blocks.

    Certainly not by humans.

    What the intervening systems bring to the table is so far beyond what you can do with the basic building blocks that is it really a completely new thing.

    That's why people work on things like these infinity categories. In one sense it is just manipulating symbols and coming up with new layers of abstraction. But when those things really work, they give you some really, really powerful tools for understanding a whole lot of other things--often in ways that just were not possible before.
    posted by flug at 11:22 PM on October 14, 2019 [6 favorites]


    How is babby formed?
    posted by syzygy at 11:53 PM on October 14, 2019


    By babbification of a prebabby.
    posted by escabeche at 6:38 AM on October 15, 2019 [3 favorites]



    Reading material:
    Lurie's "Higher Topos Theory"
    Lurie's "Higher Algebra"

    You have got to be kidding, kliuless! The first of these is 735 pages and the second one is 1553 pages.

    The illustrious John Baez writes:

    I quit working on higher categories when Lurie wrote his 735-page book Higher Topos Theory. I knew I'd have to read this book... but the mere thought of doing so made me very tired, so I switched subjects.

    And he's talking about the shorter of the two. "Higher Algebra" is more than twice that length.
    posted by crazy_yeti at 6:59 AM on October 15, 2019


    This is so dazzling and interesting, so I'm just thinking aloud here that in both computer science and computer programming, the notion of equality is not considered fundamental, in some sense. In undergraduate level Godel's proofs for first order logic, we treat equality as just another binary relation; it's not fundamental in some sense. In computer programming, things are not obviously equal and you can't take equality for granted; you have to define equality in order to use it for the data structures and algorithms you're interested in.

    And so in the OP video the speaker cracks a joke that CS people aren't mathematicians, or something.
    posted by polymodus at 7:10 AM on October 15, 2019


    By babbification of a prebabby.
    As I recall, a prebabby is just an injection from a pointed space to a contractible space, is that right?
    posted by Wolfdog at 11:18 AM on October 15, 2019 [3 favorites]


    I come from computer security, and this is how I think I've come to understand category theory.

    Are two programs the same program?

    Well, it depends how you define sameness. There's an infinite number of byte patterns that result in semantically identical outcomes. Are two programs only equivalent if their cryptographic hashes are identical?

    Sometimes yes, sometimes no. Depends how you define sameness.

    Do outcomes need to be semantically identical and indistinguishable? Or can there be irrelevant variance? Depends how you define sameness.

    Given perfect logical similarity, can we conclusively state that two programs are abstractly identical? No, one program may take a different amount of time than another to execute, or may cause another program to take more or less time to execute. Does that matter? It depends how you define sameness. Entire security models have fallen because computers have never been deterministic machines. They are only deterministically ordered, and only under very precise (usually single threaded) conditions.

    Does this matter, that computers can get faster over time? Does that mean programs are never the same, even if the stored bits never change?

    Depends on how you define sameness, equality, equivalence...category.
    posted by effugas at 10:24 PM on October 15, 2019 [2 favorites]


    « Older Irish funeral   |   Christmas comes early for Hungarian opposition Newer »


    This thread has been archived and is closed to new comments