I'm working my way through Bartosz right now, and I'm struck by how little of this category stuff feels computable. e.g. if the product in Set is defined through the universal mapping or through a limit, it still feels like you need to do infinite amounts of work to actually distinguish the product object? Am I missing something here?
I guess more generally I'm concerned about what feels like handwaving --- and I'm not sure if it's my understanding that's doing the handwaving or if it's the material itself
I feel like there could stand to be a Category Theory for Programmers that skews significantly closer to the Programmers side of things. I'm afraid Bartosz is too incurably cursed by the curse of knowledge to be able to dumb himself down the necessary amount (for me at least—though I'm always willing to give his book another try as I love his talks and personality).
Apologies if that's not what you meant by computability :) I'm out of my depth here
computability meaning, eg: the product diagrams give me a way to verify that something is a product. but there doesn't seem to be any machinery that will locate a product in a category
Not to give you any more book ideas :P But I'd love a version of a Category Theory book that explores as many possible concepts via programmatic "witnesses" (like this bit from Thinking With Types for example). This leverages my extant programming experience to catapult an intuitive understanding of isomorphisms up and over my brain walls. It decidedly does not stultify me with eldritch math symbols or lingo.
Maybe a has a canonical sum-of-products form as Either () a. This can be proven via an isomorphism:
toCanonical :: Maybe a -> Either () a
toCanonical Nothing = Left ()
toCanonical (Just a) = Right a
fromCanonical :: Either () a -> Maybe a
fromCanonical (Left ()) = Nothing
fromCanonical (Right a) = Just a
toCanonical and fromCanonical convert between Maybe a and Either () a without losing any information. This witnesses an isomorphism between the two types.
I was expecting similar examples in Bartosz's book, but alas, there weren't nearly as many as I'd hoped for. The cute little explosives-wielding piggies could only help so much.
computability meaning, eg: the product diagrams give me a way to verify that something is a product. but there doesn't seem to be any machinery that will locate a product in a category
For me that's a feature, allowing very different implementations/instances of the concept of, say, a product. Having a uniform interface for a collection of important concept that you won't be able to recognize mechanically can be /really/ useful. It's useful
especially when you apply it in the negative: showing that a certain category doesn't have products means that, no matter how much you look for it, you won't find it.
I'm working my way through Bartosz right now, and I'm struck by how little of this category stuff feels computable. e.g. if the product in Set is defined through the universal mapping or through a limit, it still feels like you need to do infinite amounts of work to actually distinguish the product object? Am I missing something here?
I guess more generally I'm concerned about what feels like handwaving --- and I'm not sure if it's my understanding that's doing the handwaving or if it's the material itself
I feel like there could stand to be a Category Theory for Programmers that skews significantly closer to the Programmers side of things. I'm afraid Bartosz is too incurably cursed by the curse of knowledge to be able to dumb himself down the necessary amount (for me at least—though I'm always willing to give his book another try as I love his talks and personality).
Apologies if that's not what you meant by computability :) I'm out of my depth here
i feel the same way --- though coming at this as a programmer :)
computability meaning, eg: the product diagrams give me a way to verify that something is a product. but there doesn't seem to be any machinery that will locate a product in a category
nobody has shown me an algorithm i can throw at a category and eventually get the product type out
short of
pick every X, A, B, Z, then pick every f:X->A, g:X->B, etc, and see if the product diagram holdsfor infinite sized things, determining the answer here is equivalent to solving the halting problem
Not to give you any more book ideas :P But I'd love a version of a Category Theory book that explores as many possible concepts via programmatic "witnesses" (like this bit from Thinking With Types for example). This leverages my extant programming experience to catapult an intuitive understanding of isomorphisms up and over my brain walls. It decidedly does not stultify me with eldritch math symbols or lingo.
I was expecting similar examples in Bartosz's book, but alas, there weren't nearly as many as I'd hoped for. The cute little explosives-wielding piggies could only help so much.
i'd pay money for that. Maybe @tel could write one
but alas he is not here
Explosive wielding piggies are really cute tho
@Sandy Maguire
For me that's a feature, allowing very different implementations/instances of the concept of, say, a product. Having a uniform interface for a collection of important concept that you won't be able to recognize mechanically can be /really/ useful. It's useful
especially when you apply it in the negative: showing that a certain category doesn't have products means that, no matter how much you look for it, you won't find it.
that's a really interesting perspective