Bravo Bartosz. All of the lectures in this series are presented in a relaxed way, but the explanation of category theory is thorough. Not being the brightest spark, I have had to watch them multiple times. You have removed much of the horror around my transition from imperative to functional programming. Thank you.
The lecture series makes much more sense when it is watched again after one has had a few months to turn the subject matter over in one's head. Thank you again Bartosz - I truly mean no offence (I mean it only as my own failing) when I say I can actually stay awake for the duration of a lecture. It must have been subconsciously absorbed the first time round.
Dear professor, Your lectures are amazing. I'm feeling the enjoyment of learning ur words bloody meanwhile my french instructor doesn't do as well as you do. you are Richard Feynman of Logic. I adore your lectures for this course. Thanks
i feel like i actually understand epics and monic now, wow. after all these years. finally!!!!!!! thank you! the most understandable category theory introduction EVER!
The passion that you manage to transmit is unbeilable, and on top of that you have a clarity that makes everything really easy to understand. Infinite thanks for taking the time to make these high quality videos and share them for free. Cheers from Argentina.
Coming from a C/C++ background I was confused at first by the fact that you cannot call a function f::void -> S since you cannot construct an element of void. I realized through that C's use of "void" is actually what he refers to as Unit soon after introducing void.
I think it's an unfair comparison because in C/C++ you have procedures, and a procedure isn't described by mappings of elements, so you really are invoking it with void. A void->void signature would imply a 'pure' procedure / side effect.
@@warwolt I totally agree. The procedures that Deaton's mentioned doesn't conform to mathematical & (to be specific) algebraic rules. Hence, the analogy is flawed.
@@warwoltI was thinking that same thing when he asked whether a function could accept a void argument: I immediately thought “Yes: That’s a procedure”. But then I realized that “procedures” as I’ve known them have no place in what he’s describing.
Looking at a morphism/function *_f_* ::A->B (in a concrete or set-like category), if *_f_* is a non-monomorphism, it's like an ABSTRACTION, because the function simplifies and ignores some differences in A. (that is, some elements that are different in A are mapped to the same element in B.) If *_f_* is a non-epimorphism, it's like MODELING, because the information in A is embedded in a more complex space in B. (That is, there are elements in B that aren't included in the image of A.) That's one of the deepest insights I've heard in any introductory Category lecture.
Hi Bartosz! Thank you very much for these classes! I have a question about the Unit type. I have some understanding of haskell so I understand well that Unit has one single value "( )". But since we are in the "Set Category" I'd like to look at that type in terms of sets. What set corresponds to the Unit? I was thinking in any "singleton set" but is it relevant that there are infinite possible singleton sets? ({0}, {1}, {2}, {10}, ...)
Do I understand correctly that being surjective and injective does not yet imply isomorphism for a function, as you would need an inverse as well? Is that also the reason why a monic and epic morphism does not imply isomorphy as you would need an 'inverse' morphism?
Injective+surjective guarantees that the inverse function exists in Set. This is not true in an arbitrary category: monic+epic doesn't guarantee that the inverse morphism exists.
Assume f is both monic and epic, then we have a diagram like this: g1 f h1 W ===> X ------> Y ===> Z g2 h2 There's no arrow Y->X in this diagram, and nothing to suggest that any should necessarily exist (let alone an inverse of f). In the case of Set, we know that morphisms that are both monic and epic correspond to bijections, and we know that bijections are invertible, and therefore we know the inverse morphism will exist. We have to use our specific knowledge of Set to arrive at this conclusion though.
An isomorphism is a bijection yes. But it is also a homomorphism. It is possible that a bijective mapping is not an isomorphism if it is not a homomorphism. Two sets are isomorphic if there exists an isomorphism
I am trying to make a parallelism with code here. I am not very familiar with Haskell, but I wanted to know if the void type and the singleton type could be translated to these pieces of code: int f(void) { return 2; // return a type } singleton g(anytype arg) { // return a singleton }
Wouldn't the definition of a void type be one that comes from void. Nothing can create void, therefore void creates void. Hence, void f(void) { return void; }
I have a question. About the monomorphism. You don't have to search through all possible c in the universe all possible pair of (g1,g2) for f to be monomorphism in the Set Category is it? I recognized that as long as c and a has one-to-ona relation then you can already check the monomorphic for f, am I right? So aside for the general category monomorphism test, you can just check it like this "For all g1,g2::a->a, f•g1=f•g2 follows g1=g2 iff f is a monomorphism." Is this a right assessment? Similarly, the test for set epimorphism can be modified as "For any pair of g1,g2::b->b g1•f=g2•f follows g1=g2 iff f is a epimorphism."
Thank you very much for these very clear and generous lectures. May I ask a question: If functions can be viewed as sets of tuples, when we consider the category "Sets", where the objects of the category represent sets, and its arrows represent functions, wouldn't functions be represented as both objects and arrows? If so, would there be anything wrong with two elements of a category (an object and an arrow) representing the same thing?
I can't quite give a good answer to this yet but what I can tell you is this: A category has Objects and Morphisms. Very often, Objects will be like set-Elements and Morphisms will be functions from one set to another. However, you can also have a category in which functions will be your objects and transformations between those functions are going to be the Morphisms. With that you also get the ability to compare two different functions and tell whether they are the same. However, at that point you have switched categories. You won't see one and the same category taking functions as both Objects and Morphisms. Unless I really got something wrong thus far. I don't have particularly deep knowledge of these topics yet. Also, if you want a preview of what's to come in this course, check out this blog bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
the bigger-than statement mainly is for when you want to talk about a "set of all sets" - That cannot happen. Instead, already in ZF set theory, such a construct is a "proper class" which is too large for any set to contain. In case of category theory, you get the category Set which is larger than any one set. At least that's my current understanding.
Even though function can be view as a set of tuple, if we look at this from a more detailed viewpoint then we should see there is no problem. Since each object is s set of elements whiles function is a set of tuples of these elements. So the meaning in the context don't collide. You don't have to worry. Relation is a kind of Set with some special property, it is a subset of a Cartesian product.
You say in category theory, we 'throw away all the information' pertaining to the inner structure of objects, however in Set, don't we have all the information about membership of the set corresponding to a given object A through the labels of all morphisms from ()->A?
Regarding the monomorphism lecture: so looking at the drawing, what changes would make f monomorphic? Changing f so that it maps to two different elements would make it injective, but then how would the equation you’re giving be fulfilled? Outcomes of invoking f two times on the results coming from g1 and g2 will give two separate elements in the set b. What am I missing here? :D
@@marekm7764 I'm not sure I understand your question. It's not an equation, it's an implication A=>B. It's negation, or counter-example, is A and not B.
Bartosz, I would like to ask you a question: in what sense "g1" is equal to "g2"? I mean, what makes them equal? Only (my assumption) the fact that they are both following the "f"? Thanks a lot for the lectures!
To get good intuitions you should try this with functions. Pick f that is not an epimorphism, for instance, f(x) = x*x. Pick g1(x) = abs(x) (absolute value) and g2(x) = x. These are two different functions, but they only differ for negative values of x. So if you apply them AFTER f, which only returns non-negative numbers, they give the same results.
@@DrBartosz Thank you for your answer! Just wanted to clear for myself: you gave me the example of functions (g1, g2) in Haskell? Just I'm actually a philosophy student, I'm pretty familiar with the java# language, but not with Haskell, so maybe you can give an example in java#/ordinary algebra, sorry for that!
@@xxxxxxxxXeroxxxxxxxx Those examples are ordinary math (but you might write x*x as x² and abs(x) as |x| instead). In Haskell syntax, it would be "f x = x * x", "g1 x = abs x" (or simply "g1 = abs"), and "g2 x = x". Mathematically, functions are mappings of values from one set (domain) to another set (codomain). Two functions f1, f2 are equal if they are the same mapping, i.e. for all elements x of the domain we have f1(x) = f2(x).
I don't agree with his description of laziness, neither here nor in his previous talks. "The empty set is not empty because it contains bottom". This is true in Haskell because laziness is a symptom of how error is treated (f error error), but in a theorum checker this would not be the case.
I should ask "which theorem checker," because every checker is based on some axioms and some model of computation. I didn't want to bore people with hard-core theory, so I just mentioned these things as curiosities. The model I'm talking about is based on Dana Scott's domain theory.
@@DrBartosz I wasn't critical about your talks, I think they're great but I just think that Haskell is a bad choice to explain maths. If you have universal laziness you have a great parsing language (like prolog) but your expressions no longer represent concrete values so it's inconsistent with maths.. :)
@@derekfrost8991 Which maths? I would ask. I think you have just one particular model of computation in mind where types are sets of values. That will work okay until you introduce recursion. If you don't like laziness, you can use Idris, which is very similar.
1:08 When you cancel the “f” it’s like saying “it doesn’t matter how we got here (the codomain of either g), because in both cases the image of f is the codomain of f. That is why f is epic.
This is a so much simpler understanding of monic and epic than I achieved from the previous video. All those terms like injective and surjective just to explain a type of purity about a function from pre-composition and post-composition
5:29 when you cancel the “f” it’s like saying “it doesn’t matter how we got here (codomain of f), because in once we’re in the codomain of f there’s only one element in the domain that could have landed us here. That’s why f is monic.
In these cases (f is monic or epic) you can compose f with any functor losslessly. Monic: pre-composition. Epic: post-composition. Isomorphism: either (and this both) composition(s).
Going back to visualizing a relationship from X to Y as a subset of the Cartesian product from X to Y, we can inspect void-> Y, unit -> Y and bool -> Y. There are 0 relations from void -> Y. There are powerset of Y relations from unit -> Y. Think of each element in the Cartesian product as a binary digit. Now every number that you can construct uniquely identifies a valid relation. There are only ||Y|| functions from unit to Y though. There are powerset ||Y||*2 relations from bool to Y. There are ||Y||^2function from bool to Y There are powerset ||Y||*||X|| relations from X to Y. There are ||Y||^||X||functions from X to Y.
Hi, Thank you for sharing ! I had some hard time trying to learn category theory but with out truly succeeding in securing my understanding. You’ve made it accessible and that is great. I have a question about the simple type, and in particular the unit type that in set correspond to the Singleton set in your exemple. I am puzzled by the fact that you said that in logic it would be the True value. I though that true corresponded to the entire set as false to the empty set. so in set theory termes the unit type is it the Singleton set or the entire set? Thank you for feedback Regards
let S been a set, a predicate correspond p:S->bool on S to the subsets {x:S | p(x)}. The false predicate defines the subset {x:S | false(x)}={} that correspond to the empty set. The predicate true will define the subset {x :S | true(x)} =S itself, I mean the “entire set” S. I would have thought that the unit type would correspond to the set S itself. I am sure I wrong but don’t know where.
I think I got a little confused by the definition of monomorphism and the relation to an injective function. A monomorphism want to be the equivalent definition in category theory of the injective property of a function right? (maybe wrong, and this is where my understanding stops)? At ruclips.net/video/NcT7CGPICzo/видео.html from the definition of monomorphism it's not clear to me how is it apparent that f is __not__ collapsing information ? if I apply f (an morphism from a to b) after g1 or g2 i always go to b (whether or not I lost information) . When is it that I do not go to b ? If I take the arrow below f? Would not that arrow have another label?
Better to say that monomorphisms "want" to define when left-cancellation can be done in equations like "f . g1 = f . g2". Injective functions just happen to be a special case of this. The notion of monomorphism was probably originally motivated by the notion of injection (don't take my word for that), but the analogy between them only works to a certain extent, because monomorphisms are just vastly more general.
How can this strong conditions for both epi and mono be fulfilled? I am especially having trouble wrapping my head around the idea of how all possible pairs of morphisms g1 and g2 can be equal under composition with f. I feel like for every pair that are equal under composition, I can come up with a pair that fails to be equal under composition with f. Someone set me straight, I'm loosing sleep over this, did we come up with a property that never holds? clearly I'm missing something here.
Something happened to me recently, one was when I heard a powerful Qur'an recitation that made my heart tremble. And the other was last night when all of a sudden the aggregated efforts and time I invested in these lectures have come to fruition . Your efforts are much appreciated my dear professor, I hope that the Almighty expands your chest.
I'm confused about the definition of monomorphism. In the diagram at 5:08, let's make g1 and g2 both map point z to x1. Now g1 and g2 are equal, the compositions "f after g1" and "f after g2" are equal, and yet "f" is still not injective. So it seems testing g1 = g2 and "f after g1" = "f after g2" (for all g1, g2, and c) is not enough to guarantee that f is injective? Where am I going wrong here?
OK I think I figured it out. It's not enough to just look at g1 = g2 and f g1 = f g2. We really must consider whether g1 may be allowed to differ from g2 while still having f g1 = f g2. If we find a pair g1, g2 where g1 = g2 and f g1 = f g2, we should also ask "hypothetically, if g1 and g2 were actually different at point z, would f g1 still equal f g2?" If yes, then f is not injective.
f :: Void -> T is defined by an empty relation(empty subset of Cartesian product of Void and T, which is also empty). absurd function is real! it is the intuition of ‘taking an element from domain and returning a corresponding element from codomain’ that lacks descriptive power, imho.
18:35 “This function must be constant, right?” Couldn’t such a function be probabilistic? Wouldn’t rand_int(), a function that returns a random integer, be such a function? If so, couldn’t we imagine an infinite number of such functions that return a Boolean (one that returns TRUE with 50% probability, another that returns TRUE with 25% probability, another with 12.5%, etc.)? Or are such functions not “pure”?
Logical proposition being true corresponds to a type being inhabited. So any type for which you can produce a value corresponds to a true proposition. Int is true because... well, zero. Bool is true because: True and False. But Void is not true, because you can't produce a value of type Void. It has no data constructor. So Void is false.
@@DrBartosz wow, never thought I got replied from you! Thanks all you have done for building such a wonderful bridge between category theory and programming.
very tiny minor nitpicking: in 6:07, "of course you can have a category with no epimorphisms, or no monomorphisms", should be something like "with no non-identity epimorphisms or monomorphisms"
Wait, so I thought monomorphism meant that f had to map "one to one"? In his example, both x1 and x2 maps to the same element, which means it's not injective at least, but can it still be monomorphic then?
8:00 TypeScript here 🙋🏻♂️ *never* type is like an empty set it is even more empty than for void, undefined and null😅, *unknown* is the set of all types and *any* is the set of all sets which is a paradox that you can resolve by thinking about *any* as being something cursed it is just like turning the type system off and you are in the voidness
If you argue that in set theory you must absolutely avoid the set of all set to be able to make a meaningful usage of the set theory… I will be happy to argue that in TypeScript you must absolutely avoid the any type to be able to make a meaningful usage of the TypeScript 😅😅😅😅
I had to do it in TypeScript and my reality does not hold *any* longer, my future is *unknown* I will *never* know: function bluff(arg: void): number { return Number(arg); }
The section about void at 9:00 was borderline philosophical, and now I'm much more interested in the simulation hypothesis. All of these might sound ridiculous or stupid but having spent almost an hour of my 10 minute lunch break I couldn't help but post them. No element of void exists because you can't create "nothing" out of "something". It doesn't exist, but we know about it because its information (e.g. its definition, effects of its non-existence, etc.) exists. It just is. By applying logic and arithmetic over its definition, we create an imperfect (as far as its information goes) replica of the void, project it into our own existence, and realize its own existence in a way. If we can draw a parallel from this to our universe, suddenly the big bang (a.k.a. "things" being created from nothing) isn't that mysterious anymore. Like void coming into "existence" in logic and math, our universe might have come into existence in the form of space and time, whilst originally being in the form of pure information. The laws of physics may prevent the creation of something from nothing, not because that's the ultimate truth, but because they've just been designed this way for this particular universe or existence. Logic and thinking can, however, give meaning to things that aren't, because the domain of information is above the domain of existence and therefore it's not constrained by its rules. As egotastical as it may sound, we might have as well just created ourselves by simply "thinking" about (cogito, ergo, sum?). What we call the universe might not even be shared at all, but rather be our own definition of existence, modeled around the concepts of space and time. And perhaps when we die, it's not our self and sentience that dies, but rather, the universe that we created becomes non-existent, so "we" just revert to our original form afterwards. So perhaps the concept of afterlife isn't just a tale, but rather a reality, just not in the way religions think. Anyway, I think I should get back to work, after all, that's what's "real", right?
Bravo Bartosz. All of the lectures in this series are presented in a relaxed way, but the explanation of category theory is thorough. Not being the brightest spark, I have had to watch them multiple times. You have removed much of the horror around my transition from imperative to functional programming. Thank you.
The lecture series makes much more sense when it is watched again after one has had a few months to turn the subject matter over in one's head. Thank you again Bartosz - I truly mean no offence (I mean it only as my own failing) when I say I can actually stay awake for the duration of a lecture. It must have been subconsciously absorbed the first time round.
Dear professor, Your lectures are amazing. I'm feeling the enjoyment of learning ur words bloody meanwhile my french instructor doesn't do as well as you do. you are Richard Feynman of Logic. I adore your lectures for this course. Thanks
"You can not construct falsity from something" ... love these gems. So much detail, even when re-watching. Great dense series. Thanks for posting.
I wish I’ve discovered this sooner, it’s a really interesting topic I’ve always been scared to dive deep into
i feel like i actually understand epics and monic now, wow. after all these years. finally!!!!!!! thank you! the most understandable category theory introduction EVER!
The passion that you manage to transmit is unbeilable, and on top of that you have a clarity that makes everything really easy to understand. Infinite thanks for taking the time to make these high quality videos and share them for free. Cheers from Argentina.
Thank you for the kind words.
Coming from a C/C++ background I was confused at first by the fact that you cannot call a function f::void -> S since you cannot construct an element of void. I realized through that C's use of "void" is actually what he refers to as Unit soon after introducing void.
I think it's an unfair comparison because in C/C++ you have procedures, and a procedure isn't described by mappings of elements, so you really are invoking it with void. A void->void signature would imply a 'pure' procedure / side effect.
@@warwolt I totally agree. The procedures that Deaton's mentioned doesn't conform to mathematical & (to be specific) algebraic rules. Hence, the analogy is flawed.
@Evi1M4chine It's an emulation of it, but it's not truly a side effect, so I will still argue for the accuracy of what void denotes in C
@@warwoltI was thinking that same thing when he asked whether a function could accept a void argument: I immediately thought “Yes: That’s a procedure”. But then I realized that “procedures” as I’ve known them have no place in what he’s describing.
12:47 Void False
13:43 proposition as a type
21:49 replace elements by morphism to a set
Looking at a morphism/function *_f_* ::A->B (in a concrete or set-like category), if *_f_* is a non-monomorphism, it's like an ABSTRACTION, because the function simplifies and ignores some differences in A. (that is, some elements that are different in A are mapped to the same element in B.) If *_f_* is a non-epimorphism, it's like MODELING, because the information in A is embedded in a more complex space in B. (That is, there are elements in B that aren't included in the image of A.)
That's one of the deepest insights I've heard in any introductory Category lecture.
And then a combination of the two becomes an ABSTRACT MODEL.
Hi Bartosz! Thank you very much for these classes! I have a question about the Unit type. I have some understanding of haskell so I understand well that Unit has one single value "( )". But since we are in the "Set Category" I'd like to look at that type in terms of sets. What set corresponds to the Unit? I was thinking in any "singleton set" but is it relevant that there are infinite possible singleton sets? ({0}, {1}, {2}, {10}, ...)
Short answer: they are all isomorphic.
and because we do not look into the sets and treat them as atomic ?
thank you again and thanks god it started with repetition of epimorphism explanation.
Do I understand correctly that being surjective and injective does not yet imply isomorphism for a function, as you would need an inverse as well? Is that also the reason why a monic and epic morphism does not imply isomorphy as you would need an 'inverse' morphism?
Injective+surjective guarantees that the inverse function exists in Set. This is not true in an arbitrary category: monic+epic doesn't guarantee that the inverse morphism exists.
Yay, learning! Thank you Bartosz. cant wait for the next issue.
But why specifically is this? Will we see examples of this later in the course?
Assume f is both monic and epic, then we have a diagram like this:
g1 f h1
W ===> X ------> Y ===> Z
g2 h2
There's no arrow Y->X in this diagram, and nothing to suggest that any should necessarily exist (let alone an inverse of f).
In the case of Set, we know that morphisms that are both monic and epic correspond to bijections, and we know that bijections are invertible, and therefore we know the inverse morphism will exist. We have to use our specific knowledge of Set to arrive at this conclusion though.
An isomorphism is a bijection yes. But it is also a homomorphism. It is possible that a bijective mapping is not an isomorphism if it is not a homomorphism. Two sets are isomorphic if there exists an isomorphism
i'm on video 2.2. these are wonderful. easy to follow. thank you for making them.
nice series, thanks for sharing!
plz :: () -> moar
I am trying to make a parallelism with code here. I am not very familiar with Haskell, but I wanted to know if the void type and the singleton type could be translated to these pieces of code:
int f(void) {
return 2; // return a type
}
singleton g(anytype arg) {
// return a singleton
}
Wouldn't the definition of a void type be one that comes from void. Nothing can create void, therefore void creates void.
Hence,
void f(void) {
return void;
}
I have a question. About the monomorphism. You don't have to search through all possible c in the universe all possible pair of (g1,g2) for f to be monomorphism in the Set Category is it? I recognized that as long as c and a has one-to-ona relation then you can already check the monomorphic for f, am I right? So aside for the general category monomorphism test, you can just check it like this "For all g1,g2::a->a, f•g1=f•g2 follows g1=g2 iff f is a monomorphism." Is this a right assessment? Similarly, the test for set epimorphism can be modified as "For any pair of g1,g2::b->b g1•f=g2•f follows g1=g2 iff f is a epimorphism."
In Set, things are simple. In fact, you can pick c to be the singleton set in the monomorphism test.
Thank you very much. So the written test of yours was for any general category. Very simple lessons about CT that cannot be fine elsewhere on YT :).
Thank you very much for these very clear and generous lectures.
May I ask a question:
If functions can be viewed as sets of tuples, when we consider the category "Sets", where the objects of the category represent sets, and its arrows represent functions, wouldn't functions be represented as both objects and arrows? If so, would there be anything wrong with two elements of a category (an object and an arrow) representing the same thing?
I can't quite give a good answer to this yet but what I can tell you is this: A category has Objects and Morphisms. Very often, Objects will be like set-Elements and Morphisms will be functions from one set to another.
However, you can also have a category in which functions will be your objects and transformations between those functions are going to be the Morphisms. With that you also get the ability to compare two different functions and tell whether they are the same.
However, at that point you have switched categories. You won't see one and the same category taking functions as both Objects and Morphisms.
Unless I really got something wrong thus far. I don't have particularly deep knowledge of these topics yet.
Also, if you want a preview of what's to come in this course, check out this blog bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
the bigger-than statement mainly is for when you want to talk about a "set of all sets" - That cannot happen. Instead, already in ZF set theory, such a construct is a "proper class" which is too large for any set to contain.
In case of category theory, you get the category Set which is larger than any one set.
At least that's my current understanding.
Wait till we talk about exponential objects.
fog (f composite g) = f(g) so even though g is a function it is also an object that can be acted upon
Even though function can be view as a set of tuple, if we look at this from a more detailed viewpoint then we should see there is no problem. Since each object is s set of elements whiles function is a set of tuples of these elements. So the meaning in the context don't collide. You don't have to worry. Relation is a kind of Set with some special property, it is a subset of a Cartesian product.
You say in category theory, we 'throw away all the information' pertaining to the inner structure of objects, however in Set, don't we have all the information about membership of the set corresponding to a given object A through the labels of all morphisms from ()->A?
Regarding the monomorphism lecture: so looking at the drawing, what changes would make f monomorphic? Changing f so that it maps to two different elements would make it injective, but then how would the equation you’re giving be fulfilled? Outcomes of invoking f two times on the results coming from g1 and g2 will give two separate elements in the set b. What am I missing here? :D
(you mean injective). It would kill this particular counter-example. If you can't find any counter-example, then f will be a monomorphism.
@@DrBartosz Not sure I understand your answer. Could you please elaborate a bit more?
@@marekm7764 I'm not sure I understand your question. It's not an equation, it's an implication A=>B. It's negation, or counter-example, is A and not B.
Bartosz, I would like to ask you a question: in what sense "g1" is equal to "g2"? I mean, what makes them equal? Only (my assumption) the fact that they are both following the "f"?
Thanks a lot for the lectures!
To get good intuitions you should try this with functions. Pick f that is not an epimorphism, for instance, f(x) = x*x. Pick g1(x) = abs(x) (absolute value) and g2(x) = x. These are two different functions, but they only differ for negative values of x. So if you apply them AFTER f, which only returns non-negative numbers, they give the same results.
@@DrBartosz Thank you for your answer! Just wanted to clear for myself: you gave me the example of functions (g1, g2) in Haskell?
Just I'm actually a philosophy student, I'm pretty familiar with the java# language, but not with Haskell, so maybe you can give an example in java#/ordinary algebra, sorry for that!
@@xxxxxxxxXeroxxxxxxxx Those examples are ordinary math (but you might write x*x as x² and abs(x) as |x| instead). In Haskell syntax, it would be "f x = x * x", "g1 x = abs x" (or simply "g1 = abs"), and "g2 x = x". Mathematically, functions are mappings of values from one set (domain) to another set (codomain). Two functions f1, f2 are equal if they are the same mapping, i.e. for all elements x of the domain we have f1(x) = f2(x).
I don't agree with his description of laziness, neither here nor in his previous talks. "The empty set is not empty because it contains bottom". This is true in Haskell because laziness is a symptom of how error is treated (f error error), but in a theorum checker this would not be the case.
I should ask "which theorem checker," because every checker is based on some axioms and some model of computation. I didn't want to bore people with hard-core theory, so I just mentioned these things as curiosities. The model I'm talking about is based on Dana Scott's domain theory.
@@DrBartosz I wasn't critical about your talks, I think they're great but I just think that Haskell is a bad choice to explain maths. If you have universal laziness you have a great parsing language (like prolog) but your expressions no longer represent concrete values so it's inconsistent with maths.. :)
@@derekfrost8991 Which maths? I would ask. I think you have just one particular model of computation in mind where types are sets of values. That will work okay until you introduce recursion. If you don't like laziness, you can use Idris, which is very similar.
1:08 When you cancel the “f” it’s like saying “it doesn’t matter how we got here (the codomain of either g), because in both cases the image of f is the codomain of f. That is why f is epic.
This is a so much simpler understanding of monic and epic than I achieved from the previous video. All those terms like injective and surjective just to explain a type of purity about a function from pre-composition and post-composition
5:29 when you cancel the “f” it’s like saying “it doesn’t matter how we got here (codomain of f), because in once we’re in the codomain of f there’s only one element in the domain that could have landed us here. That’s why f is monic.
In these cases (f is monic or epic) you can compose f with any functor losslessly. Monic: pre-composition. Epic: post-composition. Isomorphism: either (and this both) composition(s).
Going back to visualizing a relationship from X to Y as a subset of the Cartesian product from X to Y, we can inspect void-> Y, unit -> Y and bool -> Y.
There are 0 relations from void -> Y.
There are powerset of Y relations from unit -> Y. Think of each element in the Cartesian product as a binary digit. Now every number that you can construct uniquely identifies a valid relation. There are only ||Y|| functions from unit to Y though.
There are powerset ||Y||*2 relations from bool to Y. There are ||Y||^2function from bool to Y
There are powerset ||Y||*||X|| relations from X to Y. There are ||Y||^||X||functions from X to Y.
So void in C++ is actually Unit and the equivalent of Void in C++ would be
struct Void {
Void() = delete;
};
Feel free to correct me
I think you are right
Hi,
Thank you for sharing !
I had some hard time trying to learn category theory but with out truly succeeding in securing my understanding.
You’ve made it accessible and that is great.
I have a question about the simple type, and in particular the unit type that in set correspond to the Singleton set in your exemple. I am puzzled by the fact that you said that in logic it would be the True value. I though that true corresponded to the entire set as false to the empty set. so in set theory termes the unit type is it the Singleton set or the entire set?
Thank you for feedback
Regards
What do you mean by "entire set"?
let S been a set, a predicate correspond p:S->bool on S to the subsets {x:S | p(x)}. The false predicate defines the subset {x:S | false(x)}={} that correspond to the empty set. The predicate true will define the subset {x :S | true(x)} =S itself, I mean the “entire set” S. I would have thought that the unit type would correspond to the set S itself. I am sure I wrong but don’t know where.
I think I got a little confused by the definition of monomorphism and the relation to an injective function. A monomorphism want to be the equivalent definition in category theory of the injective property of a function right? (maybe wrong, and this is where my understanding stops)? At ruclips.net/video/NcT7CGPICzo/видео.html from the definition of monomorphism it's not clear to me how is it apparent that f is __not__ collapsing information ? if I apply f (an morphism from a to b) after g1 or g2 i always go to b (whether or not I lost information) . When is it that I do not go to b ? If I take the arrow below f? Would not that arrow have another label?
Better to say that monomorphisms "want" to define when left-cancellation can be done in equations like "f . g1 = f . g2". Injective functions just happen to be a special case of this. The notion of monomorphism was probably originally motivated by the notion of injection (don't take my word for that), but the analogy between them only works to a certain extent, because monomorphisms are just vastly more general.
How can this strong conditions for both epi and mono be fulfilled? I am especially having trouble wrapping my head around the idea of how all possible pairs of morphisms g1 and g2 can be equal under composition with f. I feel like for every pair that are equal under composition, I can come up with a pair that fails to be equal under composition with f. Someone set me straight, I'm loosing sleep over this, did we come up with a property that never holds? clearly I'm missing something here.
Try it with a function f that's both epi and mono, like f x = x + 1 on integers.
Do you explain in some lecture what cones are?
Yes, in the lecture on limits, but it's in the second series.
Something happened to me recently, one was when I heard a powerful Qur'an recitation that made my heart tremble. And the other was last night when all of a sudden the aggregated efforts and time I invested in these lectures have come to fruition . Your efforts are much appreciated my dear professor, I hope that the Almighty expands your chest.
I'm confused about the definition of monomorphism. In the diagram at 5:08, let's make g1 and g2 both map point z to x1. Now g1 and g2 are equal, the compositions "f after g1" and "f after g2" are equal, and yet "f" is still not injective. So it seems testing g1 = g2 and "f after g1" = "f after g2" (for all g1, g2, and c) is not enough to guarantee that f is injective? Where am I going wrong here?
OK I think I figured it out. It's not enough to just look at g1 = g2 and f g1 = f g2. We really must consider whether g1 may be allowed to differ from g2 while still having f g1 = f g2. If we find a pair g1, g2 where g1 = g2 and f g1 = f g2, we should also ask "hypothetically, if g1 and g2 were actually different at point z, would f g1 still equal f g2?" If yes, then f is not injective.
@@fhauiole The "for all" in the definition means that you have to consider all possible choices for g1 and g2.
f :: Void -> T is defined by an empty relation(empty subset of Cartesian product of Void and T, which is also empty). absurd function is real! it is the intuition of ‘taking an element from domain and returning a corresponding element from codomain’ that lacks descriptive power, imho.
18:35 “This function must be constant, right?” Couldn’t such a function be probabilistic? Wouldn’t rand_int(), a function that returns a random integer, be such a function? If so, couldn’t we imagine an infinite number of such functions that return a Boolean (one that returns TRUE with 50% probability, another that returns TRUE with 25% probability, another with 12.5%, etc.)?
Or are such functions not “pure”?
They are not pure.
I cannot understand why void is equal to falsty. Can someone give me a hint? Thanks in advance.
Logical proposition being true corresponds to a type being inhabited. So any type for which you can produce a value corresponds to a true proposition. Int is true because... well, zero. Bool is true because: True and False. But Void is not true, because you can't produce a value of type Void. It has no data constructor. So Void is false.
@@DrBartosz wow, never thought I got replied from you! Thanks all you have done for building such a wonderful bridge between category theory and programming.
very tiny minor nitpicking:
in 6:07, "of course you can have a category with no epimorphisms, or no monomorphisms", should be something like "with no non-identity epimorphisms or monomorphisms"
Wait, so I thought monomorphism meant that f had to map "one to one"? In his example, both x1 and x2 maps to the same element, which means it's not injective at least, but can it still be monomorphic then?
Peter Storm he actually says f is not monomorphic. Yeah, I was confused as well :)
8:00 TypeScript here 🙋🏻♂️ *never* type is like an empty set it is even more empty than for void, undefined and null😅, *unknown* is the set of all types and *any* is the set of all sets which is a paradox that you can resolve by thinking about *any* as being something cursed it is just like turning the type system off and you are in the voidness
If you argue that in set theory you must absolutely avoid the set of all set to be able to make a meaningful usage of the set theory… I will be happy to argue that in TypeScript you must absolutely avoid the any type to be able to make a meaningful usage of the TypeScript 😅😅😅😅
I had to do it in TypeScript and my reality does not hold *any* longer, my future is *unknown* I will *never* know:
function bluff(arg: void): number {
return Number(arg);
}
4:46 How is the condition not true? f after g1 leads to object y and f after g2 leads to object y as well.
Try working with some examples
Oh, Thank you! I did some and realized my mistake
The section about void at 9:00 was borderline philosophical, and now I'm much more interested in the simulation hypothesis. All of these might sound ridiculous or stupid but having spent almost an hour of my 10 minute lunch break I couldn't help but post them.
No element of void exists because you can't create "nothing" out of "something". It doesn't exist, but we know about it because its information (e.g. its definition, effects of its non-existence, etc.) exists. It just is. By applying logic and arithmetic over its definition, we create an imperfect (as far as its information goes) replica of the void, project it into our own existence, and realize its own existence in a way.
If we can draw a parallel from this to our universe, suddenly the big bang (a.k.a. "things" being created from nothing) isn't that mysterious anymore. Like void coming into "existence" in logic and math, our universe might have come into existence in the form of space and time, whilst originally being in the form of pure information. The laws of physics may prevent the creation of something from nothing, not because that's the ultimate truth, but because they've just been designed this way for this particular universe or existence. Logic and thinking can, however, give meaning to things that aren't, because the domain of information is above the domain of existence and therefore it's not constrained by its rules.
As egotastical as it may sound, we might have as well just created ourselves by simply "thinking" about (cogito, ergo, sum?). What we call the universe might not even be shared at all, but rather be our own definition of existence, modeled around the concepts of space and time. And perhaps when we die, it's not our self and sentience that dies, but rather, the universe that we created becomes non-existent, so "we" just revert to our original form afterwards. So perhaps the concept of afterlife isn't just a tale, but rather a reality, just not in the way religions think.
Anyway, I think I should get back to work, after all, that's what's "real", right?
Congratulations! You have just invented solipsism. (I was going to say "reinvented", but that would assume that somebody else existed.)