The Language of Categories | Category Theory and Why We Care 1.1
Vložit
- čas přidán 31. 05. 2024
- By first outlining a mathematically rigorous definition of a category, we can embark on a fascinating journey through category theory with examples from mathematics, computer science and logic.
This video establishes a good grounding for any keen mathematicians, formally trained or not, and aims to make dealing with the complicated structure of a category feel more natural. With plenty of examples to challenge your understanding, we'll venture into the incredibly abstract world of category theory.
― Corrections ―
12:04 - This should be: It is sunny ∧ (It is sunny ⇒ Bob wears a hat). The and operator ∧ typically has higher precedence than implication, so brackets must be used to ensure this proposition has the meaning I intended it to have.
― Timestamps ―
0:00 - Intro
0:58 - Definition
6:02 - Set
9:46 - Category of Proofs
16:00 - Functional Programming
18:34 - Outro
― Credits ―
All animation and voiceover created by Eyesomorphic.
Background music: 'Raindrops on glass', composed by Caleb Peppiatt.
― Further Reading ―
Category Theory, by Steve Awodey (Book) - Věda a technologie
Thanks to small, underrated and uncommercialized channels like yours, youtube is still at least a little bit of a cozy place 😊
This channel is literally just cozy math.
That's the goal :)
@@Eyesomorphic An admirable goal considering most math is taught in very stressful environments.
2024 is gonna be awesome!!!!
The year of category theory
Among many introductions to category theory I have experienced so far I feel like the one presented in this series seems to be the best. Your examples I think are far more useful for understanding this concept than standard purely mathematical introductions of categories of groups, topologies, etc that someone stuying pure maths wouldn't get much more new insight out of. Your work deserves to be appreciated
That's great to hear! I spent quite a bit of time considering which examples I wanted to cover, so I'm glad you found them useful :)
Consider how much your videos inspire people that never had the chance to study math with so much clarity and beauty, because I'm sure that's the case for a lot of people here besides me!
You give me fuel for thought and further will to get deeper into mathematics! Continue the superb work mate
That's really reassuring, I'm glad I could give you something to think about! Thanks for letting me know it helped, it really helps me make these videos :)
This is some very impressive work in presenting this concept in a very accessible way, and I love the overarching quality of the video!
That means a lot! A *lot* of time goes into making these so I'm really grateful when people enjoy them!
@@Eyesomorphic Oh, I know how much effort that takes, I'm currently writing a blog post on some theorem in topology and group theory that I formalized, and trying to explain what the theorem even means to an audience that may have never heard of what a group or a topology is *really* hard.
I also know that you learn a lot in trying to explain things, since the understanding that used to be sufficient for you to nod at the lecturer all of a sudden isn't enough to transmit that knowledge to someone else.
@@shadamethyst1258 That sounds exciting! I'd love to check it out once you're finished with it :D And very well said, being able to effectively communicate a topic to someone unfamiliar is truly the best test of personal understanding.
I have been waiting 6 months for this video!
me too!
Me too! Sorry for the rather long hiatus, I'm so happy to be working on videos again though!
This channel is a freaking banger
That's the aim!
@@Eyesomorphic keep it up man
Will this teacher finally be able to make me truly understand Category Theory? Subscribed!
I certainly hope so!
As someone raised on set theory, where logic and set theory is very big part of curriculum (maybe because of big contribution of people from my country when those branches very rapidly growing) and it is the very first thing done when you start to study Mathematics at university, I always had problem with how category is defined. And I assume there could be two approaches:
1. Ignore set theory completely and rebuild all foundations of mathematics via category theory.
2. Build category theory from set theory (I know you can't do it in ZFC, but why not in TG or MK).
While I know very little about category theory it seems that most authors prefer some monstrous middle way. Objects and arrows are introduced as if they ware non-definable like sets in set theory, but there is no effort to rewrite the foundations into pure category theory, and basically from the start category theory is using set theory even though it is not define within the realm of set theory. On the other hand nobody defines what those object and arrows are in language of set theory. So this whole definition feels to me like a school maths "definition": this is how it works, but we won't explain you what it is and how we came up to this point. So yeah, category theory may feel like "theory of nonsense" if the first definition seems completely detached from all of maths and there is not effort to establish it either as foundation or explain via already existing foundations.
Also there some small errors:
12:04 You have to put brackets somewhere because (A /\ B) => C is not the same as A /\ (B => C)
I understand what you're saying, but the audience of this video are people who haven't had much, if any, formal mathematics experience. As such, I am aiming to introduce categories such that people are comfortable seeing and using them, then later on we can explore the more foundation questions that you pose.
I must say that I object to the errors, although I really am grateful of people finding them, things do slip through! The implication point is simply a matter of convention, many authors, and certainly the ones I am used to reading, use the notation I provide here.
EDIT: I went back and see what you mean regarding the second point, and I do agree that I ought to put parentheses. I hope the narration makes it clear what the meaning is though, thanks for pointing this out!
Thanks for the comment, I'm glad to see that experienced mathematicians are also watching this video!
@@Eyesomorphic Don't get me wrong. I love your videos, I enjoy them very much and keep doing what you are doing. Also at this point I am more of an enthusiast than someone who studies mathematics and like "light" videos like those to refresh some concepts in my head. There was not jab at you, but more at the fact that your definition of category is the one that is almost always used, maybe because of how light it is, but each time I see it my set-theoretic hearth is crying. :D It maybe is my fault, because I had never had the motivation to find a book that either rewrites all foundations or builds category theory completely inside of set theory and learn the subject from it. But from perspective of a person who was interested with set theory and universal algebra I must say that category theory fells I little bit carefree when dealing with foundations. :P
I retract what I wrote about implication, because I was trying in my head to translate from Polish to English and I may have done some mistakes, including swapping relevant terms. And all that fussing about when you should use symbol => and when -> , what is implication, and what is not, what words to use, is to blurry in my memory for me to not write something accidentally stupid. :P
Im an engineer. I just love math for math's sake but I do not want to study it in a very formal way or spend years working out every small detail rigorously, even though I understand its value. In the sense of the audience you are targeting, people like me, I would also agree that the parentheses make the idea clear. That implication is not automatically a true statement.
Towards the end of the video, I was going, WTF is this? Why is he making such trivial statements that are virtually self fulfilling prophecies? But only by the end I realised that you are actually constructing the 1ST FOUNDATION STONE of the ENTIRETY of mathematics in this video, and I'm almost in tears at having understood the intuition you have tried to provide in that regards.
I agree with the others that this is the best introduction I have seen about the subject, with most people explaining how groups work and the transformations amongst them. No one has come so barebones and made me understand why category theory MUST exist.
I salute you Sir, from the deepest bottom of my heart, and its teachers like you who keep stoking the fire of our love for math, in people like us who do not necessarily burn as with and as that fire...
The examples really help to understand the concepts. I can't wait for more of these.
i absolutely LOVE this series! your presentation is simple yet striking. great work is being done here, keep it up! ❤
Another banger as usual. Good work.
Much appreciated, and nice username 👀
Yoo I've been waiting for part II for such a long time! I'm happy to support you on Patreon if that helps you upload more regularly 😃
That's really kind! I'll look into options like Patreon in the future. But currently the bottleneck isn't so much funding but rather free time! I hope to release new videos quicker than this time in the future
On par with 3B1B. Please continue.
I've watched several courses on this subject. Yours is most intelligible. Examples are very important. Hope you'll be as clear explaining functors, transformations and limits. I've stuck there )
Thank you.
Waiting for the next part in this series! This introduction is amazing, this channel is making category theory approachable!!
You have such a gift. Truly.
Absolutely stunning work here! I must congratulate you. Particularly on the conceptual flow-I appreciate how much you focus on intuition, while not being afraid to show how things work "mechanically". I really appreciate the smooth approach to the mathematics here, and with such consistently pleasing visuals. I was extremely delighted when I got the notification that there was a new video from you, and I was really not disappointed at all. Keep up the great work! I know it's a lot, but for those who see it and take it in, it is truly appreciated. ❤
I was eagerly waiting for the next video. Thanks
Interesting that there is a hunger for Category Theory. I know that mine is very from satiated, keep up the awesome work!
I just found the first video in this series a couple days ago! They are wonderful! Thank you for your efforts !
This was truly awesome, :) subscribed and waiting excitedly for the next lecture
26:41 …within a limit imposed by memory…
Thank you! This was suggestive and inspiring.
Honestly what a great video! Honestly I'm kind of annoyed about how little youtube pushed this video since it didn't even recommend this video to me. Seriously its so hard to predict what the algorithm boosts and considering that the quality of this video is so high, its so annoying that it didn't get spread more. Regardless though, really really good video as always :D and best of luck with the rest of the series - I'm quite excited.
How very kind! Luckily I don't make videos for the algorithm, I make them for myself, it's a happy coincidence if it decides other people like them too!
One more point on 'almost rigorous': What does equality of morphisms mean? What does (f.g).h = f.(g.h) actually mean? Is that something that any concrete category must explicitly provide (e.g., = on morphisms in set is when the two maps produce the same output for all inputs) and thus part of the definition of a category?
That's a great question! The way to think about equality of morphisms is thinking about equality as being _axiomatic_ . I.e. we _define_ (f.g).h to 'equal' f.(g.h), whatever that may mean. Then as long as there exists some notion of equality that aligns with these axioms in a particular structure, then it can be a category. The way to think about it is relating to abstraction from lecture 1.0. We abstract the notion of equality to just a set of axioms (associativity and identity), and only work with them to prove equalities that follow on from that. Then as you say, once we provide an explicit definition for equality that satisfies these axioms then we can be sure that all of our abstract proofs also apply to these structures with the definition of equality we defined.
As a little aside, we can actually define categories where we don't impose equality at all, but rather, we only need the arrow (f.g).h to be 'isomorphic' to f.(g.h), and the same with identity (we'll see what this means later on). These are called bicategories, and have a lot of interesting properties!
Hope that all makes sense!
@@Eyesomorphic Thank you, that's how I interpreted it as well. It is funny though, that when examples of categories are given, the objects and the morphisms are stressed, but almost never the meaning of equality of morphisms in that particular category is discussed at all - although it is part of the 'data/definition of a concrete category'. I'd understand that for the examples that are 'functions preserving structure' where morphisms are functions between sets, but for other examples, this point should not be glossed over, imo. It has confused me for a long time, until I got to terms with it a while back.
@@TheOneAnOnlyGuy What equality means is defined by the second-order logic axiomatic definition of equality, using a principle called the identity of indiscernibles. For all x, y, ((x = y) iff (for all first-order predicates φ, (φ(x) iff φ(y))). You also have to include the axiom of reflexivity. These two axioms define equality in all second-order logic systems, so this includes category theory.
Thanks a lot for your work ! Can’t wait to see the next ones !!
thank you for making these. I've been watching the Bartosz Milewski series and your series is much more efficient teaching per time.
Thank you so much for this. This really helps my research.
Glad it was helpful!
When can we get our hands on some Eyesomorphic merch?!? I'm dying for a hoodie with your logo on it 🤩
Ooh good idea!
Really looking forward to seeing more!
I’m impressed again by your videos, friend! I wonder how your style would work with other STEM or even humanities topics
He's back!
I was waiting for your video. Thank you very much for your work!
It seems you're building up for something... which reminds me of the Curry-Howard correspondence!
Hope to see your next videos soon! :)
I think you're the first person to have noticed ;) I am indeed working towards the Curry-Howard-Lambek correspondence, but we'll cover loads of other categorical concepts along the way. Thanks for the kind words!
What a pleasant and interesting video. Well done.
Fantastic video! I've wanted to learn some category theory for ages but have felt too intimidated (until now). Can't wait for the next one!
Keep at it, I find it very rewarding as a subject!
@@Eyesomorphic I understand the standard text is Mac Lane's Categories for the Working Mathematician, although I've heard good things about Riehl's Category Theory in Context. However, might you know of any other good category theory video series I can watch (at least until you put out more amazing videos)?
@@AbstractNonsense_ For a book, 'Conceptual Mathematics: A First introduction to categories' is incredibly forgiving, and I think it motivates topics before jumping into theory really well. In terms of video series, Bartosz Mileweski's category theory for programmers is a good choice. You can also find some of Awodey's lectures which i think are pretty good. Bartosz's series is probably the best video series out there currently though.
@@Eyesomorphic Thanks!
Good job! Your video is insightful and easy to follow. I wonder whether there is a rigorous distinction between a "rule of inference" denoted by - and a general implication denoted =>, I only knew tge latter, defined as "p=>q is the same as not p V q".
This is a really insightful comment, I hoped someone would ask it. They are very intricately linked, have a look at the Deduction theorem! Essentially, rules of inference are 'meta' connectives, they are rules about propositions in the logic system, but implication is a logical connective, it merely makes a new proposition from two old ones. Do check out the deduction theorem, but be careful! The deduction theorem isn't always true, it doesn't hold in some whacky systems of logic
❤ ur videos so much more than u know love ur inspiration for the first time in years
YT algo gonna pick this up any second!
So good :)
How is the category of functional programming languages different from Set? They look the same to me
They do look similar! Functional languages tend to try to mimic mathematical concepts so it's not too much of a surprise. They do differ in subtle ways, the main one being that types are emphatically not sets, sets are extremely simplistic structures that are defined entirely by their contents, but types are more complex, and shouldn't really be seen as a container of values, but more as a label by which we can differentiate different values. We'll explore these categories further, and hopefully the differences will become more pronounced as we do :)
Man you are just amazing
really cool
The math channels have spoken!
Oo! You made another video
I can’t wait to learn more! Can you recommend a book on category theory that would be this level of clarity?
They can be hard to come by, Steve Awodey's Category Theory can be good, but is quite advanced. Category theory for programmers by Bartosz Milewski is good if you aren't as comfortable with mathematics, and it's both a book and a CZcams lecture series
Eugenia Cheng's starts at this same level.
strange - youtube removed the underlining. Eugenia Cheng's book The Joy of Abstraction is what I was referring to
So Type theory can be included, right?
banger as always
Also are arrows from an object to itself that AREN'T the identity allowed? example, is f : Int -> Int, f(n) = n + 5 allowed?
Yes! We only require that one of these arrows is the identity, but there can be infinitely many arrows from an object to itself that aren't the identity.
I need more🔥
Hello. Can we apply this to linguistic science?
I believe there is research into this area, but I'm not too sure myself. But if you search this up there are a few papers which might be of interest
Is this build up for a later video on homotopy type theory?
This might crop up later on, but there is a way to go before we achieve the understanding to make this intriguing area of research feel intuitive.
@@Eyesomorphic Right. There is still more to cover about categories
lovely
Do you have any intent of working on categories in evolutionary biology?
12:04 How would the line be interpreted conventionally? From what I learned in symbolic logic, a conjunction would come to effect before a conditional.
It would read "(It is sunny and it is sunny) implies Bob is wearing a hat" here.
You are quite right, parentheses are needed to make it say exactly what I meant it to, unfortunately that just slipped by
Another fantastic video, well done!
Do you animate the entire video in manim? I'm curious how much work it is to animate the little stick figures.
Also, curious about the choice to frame composition as a "law". I would describe it as an operation on morphisms, not a property of the category per se (though of course any operation can be described as a "for all, there exists unique" property)
Thank you! The figures are animated using Pivot, all the maths is done using Manim.
Composition is indeed an operation, but I find it indicative to think of it as a law when the context is determining if something is a category. As this video was designed to convince people that these three structures are indeed categories, I wanted to make it obvious that we needed to check that they satisfied the definition, which obviously includes showing an operation on morphisms exists, and satisfies the requirements surrounding it. Hope that helps, and thanks again for the kind words!
What a great video!
I just have a smal comment to make, that what you're examplifying as "functional programming" could be better explored as Type Theory. functional programming languages don't necessarily have data types, for instance, such as Closure, or even the Lambda Calculus
I did consider this, but I was hoping this approach would make it more accessible. Keep an eye out for the next lecture, which might just be an exploration of the lambda calculus ;)
I'll definitely keep an eye out! really excited about the future of this channel and series
Are you planning on making content about category theory applied in functional programming?
This will definitely be an emphasis, but the relationship between the categories of functional languages and other Cartesian closed categories and the implications of that will be a main focus :)
@@Eyesomorphic that's good to hear. I'm asking because there's a lot of category theory out there but none of it actually shows how it applies. The closest thing is from Bartosz Milewski and Spivak but neither of them do much to really show actual application and it leads to everybody calling category theory useless
next vid when
I'm just working on it now, so hopefully not too long :)
Good reason to use postfix notation. Then you don’t need that swapping all the time for composition.
((x)f)g = (x)(f.g)
The alternative is to use arrows directed leftwards, instead of rightwards, which would match the standard notation.
Some book recommended please
I would recommend 'Category Theory' by Steve Awodey
@@EyesomorphicIs he Australian?
Finally, i Thought you left youtube
PULLBACKS
"if you know you know"
vs
id_{you know}
Please talk to dedenkin cuts please😊😊😊😊😊😊
omgomgomg
Now explain monad
Might be a bit soon for that! Once we've got some more concepts under our belt, we'll have a look at monads
very comfy to listen for sleeping
WOOWW. Can you not take a 6 months break again?
That's Manim, right? Is there any way to just pop the letters onto the screen in 1/60th of a second instead of laboriously and distractingly drawing them slowly --- it's seriously gotten really tiresome I've seen it so much, just pop the letters onto the screen in one frame. The *sliding* of variables and things is ok, so you know where they come from. And they are solid, and don't take eons to redraw