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
@@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.
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...
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. ❤
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
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.
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. In categories where arrows between two objects from a set (called locally small categories), this is pretty straightforward, as defining equality of elements in a set is well 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.
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!
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!
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
Thank you for making these videos! It’s certainly much more accessible than Bartosz Milewski’s lectures! Looking forward to more in depth lectures about how this applies to functional programming!
Thank you :) I'm currently working on the next video in this series which will cover some functional programming examples of universal construction, so keep an eye out for that!
@@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.
I just love this series tbh and I'd love to see more! Just a quick note about the logic part: when reading this sign → in a logic proposition such as "p → q", it shouldn't be read as "implies". It should only be read as "(if) p then q". Implication is just between proposition because it's a property of the sentences. E.g. you can say that "p → q" implies "p", thing you can actually verify with the proposition "p → q .→ p". But again, the newly formed proposition shouldn't be read as "p implies q, which implies p" but as "(if,) if p then q, then p". It's a technicality tbh but I do agree with Quine's thought about this, arguing that it keeps the separation clear between the interpretation of the propositions and the properties of those propositions.
Hi, thanks for the kind words and feedback! Very valid point, I personally am using the convention that implies (=>) is a logical connective and entails (⊢) is a deduction in the metalanguage. So I write: P Λ (P => Q) ⊢ Q as modus ponens. In this case implication is indeed a logical connective and can be read as such, I have seen the notation you mentioned used in some literature, and both are perfectly valid. Thanks again for the feedback :D
@@Eyesomorphic no problem and thank you for your videos! I come from philosophy hence I'm not being "fluent" with maths formalism sometimes even though I did, and still read a lot of logic, so your explanations help me a lot when studying such things.
hey this series was really good! i have a tiny quibble with your definition of category though (sorry) here it's nice to separate the definition via the distinction of stuff, structure, and property. the stuff is the objects and arrows, the structure is the composition operation and the identity arrows (and maybe the codomain/domain maps), and the property is the associativity and unit laws. (e.g. it doesn't make sense to first verify that composition is associative before verifying that some composition operation exists in Example 1.2)
Thanks! Don't apologise for giving feedback, I really encourage it :) There are so many ways of defining a category and I considered quite a few before making this video. The one I use is primarily based off of Steve Awodeys definition which I think is clear for even those with limited exposure to formal mathematics. Your example definition is nice, it is certainly a perfectly fine definition that some people may find clearer, ultimately I just went with one that was given in Awodey's book due to personal preference. Thanks again for the feedback, and I'm glad you're enjoying the series :)
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 RUclips lecture series
You should probably mention that viewers should watch your 2nd video first, since the order isn't chronological. I mean sure this video is numbered 1.1 and the 2nd video is numbered 1.0, but it's not immediately obvious and is confusing
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
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 :)
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.
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.
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 like to write proofs for facts that should be pretty simple, that unnecessarily use categories -- in that, it would be perfectly fine to prove them without categorical machinery. Is there something wrong with me?
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!
Interesting question! I'm not quite sure what you mean by unique here, but the answer is almost definitely no! An arrow can have the same domain and codomain, indeed the identity arrow must have the same domain and codomain. Additionally, two arrows can have the same domain and codomain as each other, for example the function f : N -> N, f(x) = x + 1 (where N is the set of natural numbers) has the same domain and codomain as the function g : N -> N, g(x) = 2x. Hopefully that answers your question :)
@@Eyesomorphic Thank you! I was more referring to whether an arrow "f : A-->B" can also have "C" and "D" such that "C≠A" and "D≠B" as the domain and codomain of "f" respectively. 👀
Not quite, we're defining S to be the set of all sets that don't contain themselves, i.e. every set x such that x is not in x. Then asking whether S is in that set gives rise to the paradox, if S is in S then S is not in S, otherwise if S is not in S then by construction S must be in S. Hope that makes sense
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
Thanks to small, underrated and uncommercialized channels like yours, youtube is still at least a little bit of a cozy place 😊
>uncommercialized
>already a patreon
>already shitty merch
Yeah I enjoy your uncommercialized channel while it lasts lmao
@@paulmccartney2327 He gotta eat.
@@paulmccartney2327 yeah my bad. I meant not uncommercialized, but the author's priority is content, not money
@@paulmccartney2327 not you greentexting on RUclips
This channel is literally just cozy math.
That's the goal :)
@@Eyesomorphic An admirable goal considering most math is taught in very stressful environments.
@@Wizard_Pepsi And not very effectively. I'm learning far more from this than I ever did at school. Standard teaching techniques need to change.
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 :)
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.
@@Eyesomorphic In brief: if you can't explain it, you don't understand it.
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
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! ❤
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...
Will this teacher finally be able to make me truly understand Category Theory? Subscribed!
I certainly hope so!
Waiting for the next part in this series! This introduction is amazing, this channel is making category theory approachable!!
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. ❤
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
Another banger as usual. Good work.
Much appreciated, and nice username 👀
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.
I was eagerly waiting for the next video. Thanks
thank you for making these. I've been watching the Bartosz Milewski series and your series is much more efficient teaching per time.
On par with 3B1B. Please continue.
Interesting that there is a hunger for Category Theory. I know that mine is very from satiated, keep up the awesome work!
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. In categories where arrows between two objects from a set (called locally small categories), this is pretty straightforward, as defining equality of elements in a set is well 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.
This is simply beautiful....a work of art ,I must say.
He's back!
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!
I just found the first video in this series a couple days ago! They are wonderful! Thank you for your efforts !
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!
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
Impossible not to subscribe. Outstanding content. Thank you.
When can we get our hands on some Eyesomorphic merch?!? I'm dying for a hoodie with your logo on it 🤩
Ooh good idea!
Thank you for making these videos! It’s certainly much more accessible than Bartosz Milewski’s lectures! Looking forward to more in depth lectures about how this applies to functional programming!
Thank you :) I'm currently working on the next video in this series which will cover some functional programming examples of universal construction, so keep an eye out for that!
I’m impressed again by your videos, friend! I wonder how your style would work with other STEM or even humanities topics
Thank you! This was suggestive and inspiring.
Thanks for sharing this, waiting for the next video in the series!
You have such a gift. Truly.
YT algo gonna pick this up any second!
This was truly awesome, :) subscribed and waiting excitedly for the next lecture
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!
This guy is gonna get famous, I know it
I just love this series tbh and I'd love to see more!
Just a quick note about the logic part: when reading this sign → in a logic proposition such as "p → q", it shouldn't be read as "implies". It should only be read as "(if) p then q".
Implication is just between proposition because it's a property of the sentences. E.g. you can say that "p → q" implies "p", thing you can actually verify with the proposition "p → q .→ p". But again, the newly formed proposition shouldn't be read as "p implies q, which implies p" but as "(if,) if p then q, then p".
It's a technicality tbh but I do agree with Quine's thought about this, arguing that it keeps the separation clear between the interpretation of the propositions and the properties of those propositions.
Hi, thanks for the kind words and feedback! Very valid point, I personally am using the convention that implies (=>) is a logical connective and entails (⊢) is a deduction in the metalanguage. So I write: P Λ (P => Q) ⊢ Q as modus ponens. In this case implication is indeed a logical connective and can be read as such, I have seen the notation you mentioned used in some literature, and both are perfectly valid. Thanks again for the feedback :D
@@Eyesomorphic no problem and thank you for your videos!
I come from philosophy hence I'm not being "fluent" with maths formalism sometimes even though I did, and still read a lot of logic, so your explanations help me a lot when studying such things.
The math channels have spoken!
Really looking forward to seeing more!
Thank you so much for this. This really helps my research.
Glad it was helpful!
Thanks a lot for your work ! Can’t wait to see the next ones !!
26:41 …within a limit imposed by memory…
What a pleasant and interesting video. Well done.
Oo! You made another video
hey this series was really good! i have a tiny quibble with your definition of category though (sorry)
here it's nice to separate the definition via the distinction of stuff, structure, and property. the stuff is the objects and arrows, the structure is the composition operation and the identity arrows (and maybe the codomain/domain maps), and the property is the associativity and unit laws. (e.g. it doesn't make sense to first verify that composition is associative before verifying that some composition operation exists in Example 1.2)
Thanks! Don't apologise for giving feedback, I really encourage it :)
There are so many ways of defining a category and I considered quite a few before making this video. The one I use is primarily based off of Steve Awodeys definition which I think is clear for even those with limited exposure to formal mathematics. Your example definition is nice, it is certainly a perfectly fine definition that some people may find clearer, ultimately I just went with one that was given in Awodey's book due to personal preference.
Thanks again for the feedback, and I'm glad you're enjoying the series :)
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 RUclips 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
You should probably mention that viewers should watch your 2nd video first, since the order isn't chronological. I mean sure this video is numbered 1.1 and the 2nd video is numbered 1.0, but it's not immediately obvious and is confusing
another deduction identity
If True then X
True therefore X
True => X
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
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 :)
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.
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.
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
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
I like to write proofs for facts that should be pretty simple, that unnecessarily use categories -- in that, it would be perfectly fine to prove them without categorical machinery. Is there something wrong with me?
Do you have any intent of working on categories in evolutionary biology?
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!
Man you are just amazing
Loves!!!
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
So good :)
really cool
Some book recommended please
I would recommend 'Category Theory' by Steve Awodey
@@EyesomorphicIs he Australian?
So Type theory can be included, right?
12:09 You completely skipped over the order of operations here. why is it not (sunny ^ sunny) => hat ?
Yes you are quite right, unfortunately this slipped by. I clarified it as a correction in the description once I became aware
2:04 what previous lecture?
next vid when
I'm just working on it now, so hopefully not too long :)
"if you know you know"
vs
id_{you know}
Finally, i Thought you left youtube
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
PULLBACKS
I have a quiestion. Is the domain and codomain of an arrow unique? 👀
Interesting question! I'm not quite sure what you mean by unique here, but the answer is almost definitely no! An arrow can have the same domain and codomain, indeed the identity arrow must have the same domain and codomain. Additionally, two arrows can have the same domain and codomain as each other, for example the function f : N -> N, f(x) = x + 1 (where N is the set of natural numbers) has the same domain and codomain as the function g : N -> N, g(x) = 2x. Hopefully that answers your question :)
@@Eyesomorphic Thank you! I was more referring to whether an arrow "f : A-->B" can also have "C" and "D" such that "C≠A" and "D≠B" as the domain and codomain of "f" respectively. 👀
not sure which previous video is referenced here. can you help?
It should be linked in the description, but here it is anyway: ruclips.net/video/DrldYpmwN5s/видео.html
2:54 did you mean domain of A and codomain of C? you said domain of f and codomain of g instead
It does indeed have A as it's domain, but I was saying that this is the domain of f, as dom(f)=A. Hope that clears things up
@@Eyesomorphic Ah gotcha. Thanks
Please talk to dedenkin cuts please😊😊😊😊😊😊
At 5:32, the Russell's Paradox's fomula is wrong, should be S = {x|x
otin S}
Not quite, we're defining S to be the set of all sets that don't contain themselves, i.e. every set x such that x is not in x. Then asking whether S is in that set gives rise to the paradox, if S is in S then S is not in S, otherwise if S is not in S then by construction S must be in S. Hope that makes sense
@@Eyesomorphic Oh, you're right. I understand now.
very comfy to listen for sleeping
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
omgomgomg
🎉🧡✅👍🙏
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