∞-Category Theory for Undergraduates

At its current state of the art, ∞-category theory is challenging to explain even to specialists in closely related mathematical areas. Nevertheless, historical experience suggests that in, say, a century’s time, we will routinely teach this material to undergraduates. This talk describes one dream about how this might come about - under the assumption that 22nd century undergraduates have absorbed the background intuitions of homotopy type theory/univalent foundations.
Slides can be found here: www.math.jhu.ed...

[@jontedeakin1986]

it's *my* sleepover and *I* get to pick the movie

[@columbus8myhw]

"I might turn off the recording, if I can figure out a way to do that" is, in retrospect, a pretty funny way to end a video

[@enderwiggins8248]

This is also really interesting to me from a pedagogical standpoint; tying it to paradigm shifts in physics in the twentieth century, It's abstractly kind of funny the _lack_ of emotional impact a lot of quantum mechanics has on undergraduates. When we studied tunneling through 1D stepwise potentials, no one was flipping the tables in disbelief; and when we studied the derivation of the uncertainty principle the vibe was very "okay neat, but I kinda already knew this intuitively". I think my generation of college students has been fed a cultural diet of quantum weirdness so much that now we're unfazed by it. Maybe this is the future of ∞-category theory, that proofs that now seem so wild will seem very intuitive for college students in a century.

[@lukasjuhrich503]

For anyone looking for this as well, the result she mentions regarding „Indiscernibility of identicals“ most likely is M.Hofmann and T.Streicher: “The groupoid model refutes uniqueness of identity proofs” from the 9th annual IEEE Symposium on Logic in Computer Science. DOI: 10.1109/LICS.1994.316071.

[@miguelamaral9642]

Well as a current undergrad, I definitely did not catch everything you talked about, but awesome stuff, I look forward to learning more in the future. Cheers!

[@emilyriehl1044]

It's important to note that this is all still under development. Come back in 2120 and I bet this will all seem much clearer.

[@harriehausenman8623]

@@emilyriehl1044 And you will either be mentioned in every (probably virtual) text book or your brain matrix is much copied :-)

[@TimothyOBrien6]

@@emilyriehl1044 do you expect that the underlying logic or path of reasoning to develop these concepts is much simpler than currently understood? Is that why it will be simpler in the future, or other reason(s)?

[@GeorgWilde]

@@emilyriehl1044 Constructivists don't believe in time travel though.

[@lopezb]

Her enthusiasm is infectious!

[@Alberiana]

Thank you for this! Finally got to know what homotopy type theory might be about.

[@jsmdnq]

The big issue in modern mathematics is that there are so many different explanations and languages for the same thing. Even advanced mathematics has this issue. EVEN mathematics that are suppose to solve the problem end up contributing to it. It's much like the issue, say, with programming languages. There are thousands of them and they all purport to solve some problem but end up just adding another language to the bunch and since it actually lacks something in some other areas it never replaces everything. Category theory is essentially a unifying language that could be the theory of everything but people need to start trying to optimize and prune it and create a curriculum for all levels that are based in category theory. This way we all have the same language to use to describe things and we learn it from the start. I mean, really there is only one language with many sub-languages. The problem is there is a ton of overlap and a ton of isomorphic and equivalent structure... so much so we need a whole damn new language to get a handle on it(e.g., category theory).

[@kaushaltimilsina7727]

Nice introduction to the ideas, especially to me since I am currently studying Programming with Categories and will be studying homotopy type theory. Homotopy type theory and Category theory blended together seems like a great way to implement many ideas from pure mathematics like Homotopy theories on Schemes (which I can sort of speculate and try implementing in haskell) and many other ideas. Such ideas will probably allow great representation power (condensed representation and computation) and I speculate that in the future computation will use many ideas from pure mathematics. Also, the coloring is the really cool; it's like a really fun book. Thanks for sharing a recording of the talk. I first came across infinity groupoids when watching discussions of Wolfram Physics Project on youtube, and they were using the idea for paths in spacetime in the discussions-viewing spacetime from Homotopy Type Theory- who observes what and who can prove certain equivalences (who = which observer). It was quite fun to watch.

[@ymaysernameuay1113]

I don't know how I got here but I'll stick around.

Question at 16:56 is asking about if context morphism capital Gamma can be regarded as a formal grammar. I believe yes, I think there could be an abstract formal language grammar Gamma of which words are tuples of types. It might exist only theoretically as such formal language is extremely expressive and also contains words which are not computable. An example of that could be a type being a Turing Machine that ends. I think this question was extremely interesting, maybe just not formulated properly.

[@kitconnick427]

I didn't realise you had a channel! I remember your Numberphile videos on the marriage matching up problem, and it was always one of my favourites, you were always wonderful to listen to! Now I'm 4th year at Uni this is an interesting video in a different way. Thanks for this great and helpful video, look forward to looking at your other videos :)

[@sebastianmullerbalcazar6229]

totally agree...actually thinking conceptualy about relations make absolute sense to start understanding....everything else.

[@defamationlaw]

Love watching you teach Emily. Hello from Oz

[@miguelamaral9642]

41:17 Wow okay, beautiful picture to visualize how two proofs of the same identity type may not be equal. What then could be an interpretation of the "holes" that are preventing "homotopy" (keeping in analogy) between proofs in type theory? It is interesting to think of what could be fundamentally different about two proofs about same thing.

[@emilyriehl1044]

Here's a fun example to think about: can you think of two different proofs that "(P and Q) implies (P or Q)"? Now imagine that P and Q are single-point spaces (or better: contractible spaces, if you know what that means). Can you identify the space corresponding to "(P and Q) implies (P or Q)"? And if so, do these proofs lie in the same path component?

[@marshacd]

@@emilyriehl1044 Great reply! For me, the question at 35:37 is most important.

[@marshacd]

Also the contractible/path-connected question at about 50:45.

[@columbus8myhw]

@@emilyriehl1044 It seems to me that (P and Q) should be a one-point space, (P or Q) should be a two-point space, and the implication should be a 2^1 point space

[@AliceB0]

I just came back from work and apparently didn't close youtube or turn of my pc. I just turned on my screen 50 minutes in and have no idea what you're talking about but it sounds very interesting!

[@AdrienLegendre]

Emily, you are an excellent teacher.

[@lathspelz]

Thanks.

[@NNOTM]

Re: it being surprising that path induction works - I think it's not at all surprising in intuitionistic type theory, where our introduction rule only admits refl. It becomes surprising though once you have the homotopical interpretation and allow non-reflexivity paths.

[@DanielDugovic]

Thanks for this extraordinary lecture which lays out (I think?) a practical grammar for unit testing and integration testing! (My mathematics knowledge is limited.)

[@columbus8myhw]

I keep on confusing a definition of a type for a claim that the type is inhabited.

[@kingyinyan254]

Thanks for this very nice intro. I'm self-taught, and I'm struggling to learn more of the frontier research in categorical logic / type theory to apply to artificial intelligence. I've found a way to transfer the categorical structure of logic to deep learning that leads to programs that can be implemented and they are extremely useful in AI.

[@abj136]

This sounds exciting. I'd love to learn more!

[@kingyinyan254]

@@abj136 It actually goes by Curry-Howard correspondence. The AI system is a discrete-time dynamical system with transition function F implemented as a deep neural network. The system has to think logically, ie, the transition function should obey rules of logic. In other words, F = "⊢" in logic. So far I have only used the fact that logic conjunction A∧B is commutative. This leads to the requirement that the neural network must be "symmetric" in its inputs, ie, permutation invariant. Such neural networks has been invented around 2017 (not by me). One thing very surprising is that Google's BERT model, which is current state-of-the-art in natural language processing, is also permutation-invariant. This fact is not explicit in their paper, and it seems to support my view that AI should have "logical structure". I'm eager to transfer more of the structure of categorical logic to deep learning... the advantage of topos logic is that everything is expressed via morphisms, adjunctions, compositions, etc, and these are easier to implement as neural networks. In general it is very hard to impose structure on neural networks because they have their own very rigid structure already... :)

[@Apocalymon]

Hmm, I wonder if higher category theory can be used to advance the Wolfram Hypergraph Physics Project. Have you considered contacting Jonathan Gorard to discuss the application of category theory to the physics project?

[@keithwynroe8996]

Fantastic talk, thanks so much! Do you think this work of putting math on different foundations will be mainly valuable from a “different perspective” perspective (e.g makes it easier to engage w/ topics like infinity-categories more readily), or do you think it’s also in some way “better” than the ZFC foundations?

[@nilp0inter2]

Thank you!

[@korigamik]

is this click bait? the infinity isn't supposed to be there

[@morkovija]

Question from the mathematically-challenged audience: do you think there are things that you will never be able to understand that is understood by other scientist, or is it just a matter of time, grinding away and attacking the problem from different angles?

[@tpog1]

Thank you very much for this excellent talk! It helped me a lot to bridge the gap between normal type theory and hott. May I ask you which hard- and software you created your beautiful slides with? I was thinking about getting a Remarkable 2 but whatever you‘re using seems to be a great alternative, especially due to color support.

[@charolastrauno]

Probably Notability on ipad or mac

[@bonniewilson9709]

Accually I graduated with full honors thank you and paid out for it...cap and gown

[@kingyinyan254]

I'm wondering if one could say that fuzzy logic lives on HoTT level 2 (ie the level of sets) The rationale being that mere propositions have *binary* truth values because their proofs are considered identical so a mere proposition either has a proof or not have one but a fuzzy proposition can have a bunch of proofs (witnesses) and the number of supportive vs unsupportive witnesses (and their ratio) determines its fuzzy truth value It is actually my conviction that this should work out and that binary logic would be a limiting case of fuzzy logic And I wonder if this fuzzy interpretation might give a different structure to types as topological spaces?

[@anarchocommunist3888]

im so high how did i get here

[@dumbledorelives93]

I'll be honest, I kind of self teach myself a lot of higher level math concepts for fun, and even certain really abstract stuff I can wrap my head around, but honestly I can't understand a word of this. I feel like I'm listening to a computer talk to other computers. Is there anyone who can help me understand what the hell a type is and what these rules even mean in English?

[@b43xoit]

So math can be founded without reference to ZFC?

[@EmptyKingdoms]

Dear Emily. How would you suggest I, a literary studies' scholar, start understanding HoTT? I read the n-cat blog frequently, but it just doesn't seem to enter into my head (considering the furthest I've gone mathematics-wise is high school level). Thank you in advance.

[@-minushyphen1two379]

To study category theory, you could try The Joy Of Abstraction by Eugenia Cheng, it assumes pretty much no maths background

[@nonthakornboonrakchat5435]

Thanks XD

[@StephenPaulKing]

The HoTT concept seems to have adopted a Process ontology instead of a Substance ontology. Hooray for Heraclitus!

[@ipudisciple]

I understood almost all of the talk but almost none of your comment. Is it explainable to a philosophy noob?

[@yabdelm]

Beginners to math: run!! Not for beginners! General Semantics... wish it was applied in complex topics like these.

[@dumbledorelives93]

Yeah I'm kind of self teach myself a lot of higher level math concepts for fun, and even certain really abstract stuff I can wrap my head around, but honestly I can't understand a word of this. I feel like I'm listening to a computer talk to other computers.

[@98danielray]

​@@dumbledorelives93This is pretty much a template of higher math. what would be the "lots of higher math" you teach yourself then?

[@miguelamaral9642]

At 23:04 is there a better way to write out applying the function (pr_2(x)) on (pr_1(x))? It just seems clunky and took me a minute to parse through and indeed see it was apply a function of type P->Q for some term x of type P, and thus indeed you get a term of type Q. Thanks :)

[@emilyriehl1044]

It is clunky for sure but I'm not sure whether any other notation would be clearer. The convention to write "f(p)" for the application of a function f : P -> Q to a term p : P is so well-established. But I'm glad to hear you were able to work it out eventually.

[@corlaez]

I love your work Emily! I found Lawvere Theory very interesting kzbin.info/www/bejne/iaTbY5KAgNV1abc I wonder if there is a more principled way of combining the notion of Lawvere theory with the notion of "where" a computation should take place (in which thread). A talk on The Scala library cats-effects uses a function "shift" to change where the computation should happen: kzbin.info/www/bejne/nZDNgWdtfaujjaM

[@yoananda9]

This is for undergraduate of Vulcan's maybe, but I doubt (I'm graduate) it will work on earth. (but I agree we should try) I was expecting examples with oranges and apples and bags. (or Sets and Nats) This is FAR MORE abstract than any non mathematician can handle. Can we prove 2+2=3+1 with homotopy theory ? how ?

[@geometerfpv2804]

They said the same thing about group theory for ages.

[@Treebark1313]

programming is an excellent introduction to a lot of category- and type- theoretic concepts. imho dr riehl's estimate of 100yrs is very conservative, it could happen in a few years if the idea takes root. edit - and no less abstract than a typical intro to proofs class (into which many schools enroll freshman)

[@98danielray]

math undergraduates, obviously

[@shortnotes-bds2621]

Can you start an online lecture series on abstract homotopy theory in your free time maybe.

[@jsmdnq]

Lemma: let x and y be two possibly different things but since they are in our pre-oo-category x = y.

[@StephenPaulKing]

Category theory should be taught in High School!!!!

[@StephenPaulKing]

You might like the paper "Computing with Space" by Marius Buliga! arxiv.org/abs/1103.6007

[@imrematajz1624]

I sense a connection with how sub-Planckian distances (energies) can be computational units and defined on P-adic spaces.

[@StephenPaulKing]

The process of obtaining isomorphisms are equivalent to identities" Looks like a fixed point theorem, no?

[@myexflower]

I love you Emily, but I did not like the slides.

[@harriehausenman8623]

Yeah, they were pretty messy for 21st century.

[@giuliocasa1304]

At 17:00 about "a consistent theory of sentences" she says she doesn't know what it means?!? And she was speaking about dependent type theory. It looks like she doesn't really know what she's speaking about. And it reinforces my feelings about homotopy type theory: it produces mental confusion.

[@bogdansimeonov4999]

she's a homotopy theorist, not a logician, and this talk is clearly meant to be from a mathematician's perspective. In the beginning, she even makes it clear that she was speaking as an outsider to the field of logic

[@giuliocasa1304]

@@bogdansimeonov4999 logic is a fundamental part of mathematics that is definitely a prerequisite to type theory. And, as you can read even e.g. in nlab: "Type theory and certain kinds of category theory are closely related. By a syntax-semantics duality one may view type theory as a formal syntactic language or calculus for category theory, and conversely one may think of category theory as providing semantics for type theory."

[@bogdansimeonov4999]

@@giuliocasa1304 I am aware of the relationship between type theory and category theory, for instance how cartesian closed categories correspond to the simply typed lambda calculus. However, bear in mind that category theory arose in algebraic topology and there are still many category theorists today whose work mainly relates to topology, and not so much categorial logic. It is a very strange coincidence that homotopy theory and type theory intersect in the way HoTT describes. With this in mind, it is nice to see that mathematicians in the field of topology are interested in HoTT, but from what I understand, HoTT is basically intuitionistic type theory equipped with topological semantics, and it is fairly natural that mathematicians (algebraic topologists) will be more interested in the semantics and constructing (higher-categorical) models of HoTT rather than in its proof theory. You might be more used to the logical side where terminology like "consistent theory of sentences" is obvious, but logic has, unfortunately, been a bit insular in how it relates to the rest of mathematics. I find it nice that a field like HoTT brings both logicians and algebraic topologists alike, and we should not expect people on both sides to be equally versed in each other's terminology.

[@moter2179]

All I got from the first 10 mins was people who do math don't know set theory lol I mean the instructor is clearly knowledgable but I wish she was able to explain it better?! I dunno. Good effort still. (math grad student)

[@primefactor5417]

Dr.Emily you are so beautiful .... can you make an introductory course on category theory ?

[@bhz8947]

I’m only seven minutes in, and already the mumbled discursions upon discursions are starting to grate. Cut a straighter path when explaining something new.

[@pmcgee003]

Let's complain about your free access to a great mathematical mind. 👍

[@CosmiaNebula]

Well, I look forward to having you as my professor in 200 years.

[@tobyaldape9885]

Amazing introduction to HOTT! I loved the color coding of different "types" of objects. Helpful for math as well as programming. Keep up the good work!

[@harriehausenman8623]

Thank you so much! How is it, that you make such a complex topic more accessible than most Profs manage to do with simple calculus? :-))

[@henryrubenfischer]

At 35:05 you say it's possible to do this with a single path induction. Do you mean that after the first path induction you can just apply the Lemma that was proven directly above? (I'm asking because in the Lemma above there's a second path induction involved). Or is there some other way still to do this with the definitions in your slides?

[@davidlapidson4992]

gut

[@jamesreilly7684]

Adding "for undergraduates" as a part of a title is instantly an alarm bell for Rube Goldberg-like science (or in this case math). I have reviewed several category theory presentations and it seems to me that the ONLY thing that is new about it is the notation. Most CS already implements category theory on a daily and both explicit and implicit basis. I have yet to hear any cogent explanation of Category Theory and its application that makes any sense outside of cs whatsoever. If someone could write up a one paragraph description of category theory and why it is important I would be amazed.

[@maxh5861]

category theory is central in modern algebra, algebraic topology, and algebraic geometry. clearly you have no experience in those subjects, but you have the overconfidence to claim category theory is pointless outside of computer science

[@jamesreilly7684]

@@maxh5861 It could also be claimed as central to cs. But that is a meaningless claim. You know what is also central to all of these? Alphanumeric characters. Category theoy does not appear to add any new insights or tools for cs. Or if it has, the Acid test is whether it is used. The presentations on CT are similar to arguments for strong typing in interpreted languages. Ie polishing the turd

[@maxh5861]

@@jamesreilly7684 Theorems in CT: Freyd-Michell embedding theorem, Yoneda lemma (generalizes Cayley theorem and many similar results), Giraud’s theorem characterizing Grothendieck toposes,... I am getting the impression you’ve never heard of basic stuff like Hom-tensor adjunction CT came from algebraic topology, beginning with informal notions of “functors” and “morphisms of functors” which are impossible to understand well without the formalisms of CT. If you are wondering what’s the use for all this mathematics, ask a theoretical physicist. Computer science is not a fundamental natural science the way physics is, so it seems illogical to me that math would need to be useful to computer science in order to be valuable knowledge Do you even know how CT is applied to CS anyways? Do you know the difference between a monoid and monad and how to program in a functional language? If not, worth looking into It’s not like I’m an expert in this stuff but if you want people to think you’re a Really Smart computer science guy then you’d best stop criticizing the whole existence of fields you’re ignorant in, it’s not a good look

[@98danielray]

​@jamesreilly7684 either way, whatever pragmatic concerns you have do not apply to AG or AT, because these are theoretical by construction and category theory is imbued in their theoreticsl framework. It is naturally distinct from a mathematician trying to formalize computation. that said, the "polish" applies much more heavily to CS than CS-adjacent areas like software engineering that are frequently not distinguished from CS itself, which I suppose is what you are doing

[@kinbolluck476]

Mmm sausage