this series was perfect :) Can you consider doing a series like this for Homotopy Type Theory - especially focusing on how it can be applied in programming and automatic theorem proving ? It's find to find someone who can explain this stuff so well :))
In the beginning of you lectures, with all the directed graphs business, I was asking myself a question - "does it all have some kind of connection to topology?". When you started talking about "cells", I thought "hey that looks like simplicial complexes and algebraic topology", and then you connected to homotopy type theory and groupoids. Very nice set of lectures indeed. Thanks for all your work! Still watching and rewatching them, to better grasp all the concepts :).
Regarding the diagram at 27:41 in the middle of the board, why does F and F' both transform C into D? I think the image of C under different functor should be different, right?
Yes, we have a Russel's paradox, if we're not careful. One way around it is to work with a category of small categories (which itself is not small). Another is to introduce a hierarchy of Grothendieck universes: ncatlab.org/nlab/show/Grothendieck+universe
At 31:21 we define a natural transformation from C to E using alpha and beta. Why is this well defined? It's not obvious why every functor from C to E should be decomposable into two components C->D->E which seems to be needed to use alpha and beta.
This might seem like a silly question (my ignorance is sincere), but I'm wondering why Cat needs to be a "two-category". Why wouldn't one simply represent functors as categories of Cat, and natural transformations as morphisms of cat?
Starting from "Cat is a category of (small) categories", means its *objects* must be categories, and so its morphisms are Functors. Natural Transformations, then, are morphisms between its morphisms. So, to include natural transformations, Cat must be a 2-category.
Apologies Bartosz for interrupting and uploading personal images without permission, it was unwise, found representative the fact that while others keep the mystery behind the magic until Banach-Tarski like paradoxes appear you explain us how and why there's a ball flying in nowhere and how we can use it, sorry if it was inappropriate
please never stop making these
this series was perfect :) Can you consider doing a series like this for Homotopy Type Theory - especially focusing on how it can be applied in programming and automatic theorem proving ? It's find to find someone who can explain this stuff so well :))
In the beginning of you lectures, with all the directed graphs business, I was asking myself a question - "does it all have some kind of connection to topology?". When you started talking about "cells", I thought "hey that looks like simplicial complexes and algebraic topology", and then you connected to homotopy type theory and groupoids. Very nice set of lectures indeed. Thanks for all your work! Still watching and rewatching them, to better grasp all the concepts :).
"Very nice set of lectures."
I would rather say "Very nice category of lectures." :P
A very nice natural transformation from set to category :)
@@clementdato6328 even better
If every morphism is invertible, doesn't that make all the objects the same up to isomorphism?
Such an amazing lecure. You are a great teacher! Thanks for making all this content for free
Regarding the diagram at 27:41 in the middle of the board, why does F and F' both transform C into D? I think the image of C under different functor should be different, right?
Thank you a lot for the lectures, Dr. Milewski!
Thank you for extracting the essence of HTT in this installment.
Cat ( the Category of categories) is an object in Cat? Do we have similar to Russels paradox here? Please explain.
Yes, we have a Russel's paradox, if we're not careful. One way around it is to work with a category of small categories (which itself is not small). Another is to introduce a hierarchy of Grothendieck universes: ncatlab.org/nlab/show/Grothendieck+universe
At 31:21 we define a natural transformation from C to E using alpha and beta. Why is this well defined? It's not obvious why every functor from C to E should be decomposable into two components C->D->E which seems to be needed to use alpha and beta.
All four functors and two natural transformations are given as inputs.
Isomorphisms are defined using equality, though, so can you ever escape it?
Correct. We can push it deeper and deeper, though. Eventually we reach infinity-categories.
This might seem like a silly question (my ignorance is sincere), but I'm wondering why Cat needs to be a "two-category". Why wouldn't one simply represent functors as categories of Cat, and natural transformations as morphisms of cat?
Starting from "Cat is a category of (small) categories", means its *objects* must be categories, and so its morphisms are Functors. Natural Transformations, then, are morphisms between its morphisms. So, to include natural transformations, Cat must be a 2-category.
Mind = Blown !
Awesome as always!!
13:33 cells interlinked
That moment when you keep abstracting category theory and realize you ended up back at graph theory.
good lecture, please do not stop!!!
My simple self says cat is a cute pet.
>''< is not double prime but secunda (''' is tercia and so on)
Apologies Bartosz for interrupting and uploading personal images without permission, it was unwise, found representative the fact that while others keep the mystery behind the magic until Banach-Tarski like paradoxes appear you explain us how and why there's a ball flying in nowhere and how we can use it, sorry if it was inappropriate
only 126 knows how things works
Lost in translation again, founded=found, i've to go back with the english book, sorry again
Ok, I founded, Hexation, sorry... Lost in traslation with sexagesimal :)