Is there a good "entry point" to category theory from a software developer background ? I'm trying to learn category theory concept but it's a bit "abstract", I mean there are several good video on youtube, there is the maclane book but I miss a way to "exercise" it and have the result checked
the best book for programmers to learn about category theory is in my opinion Algebra of Programming by Bird and de Moor
will have a look
thank for the suggestion
they focus mostly on (1) the category of sets and total functions and (2) the category of sets and relations, but unless you're doing fancy stuff, these are in my opinion the core ones, where one can actually use category-theoretic results to get work done, e.g., fusion theorems
Haskell's category of cpos and partial functions is from my view mostly a weird distraction
Benjamin Pierce's Category theory for computer scientists is usually mentioned when this topic is raised, but I wasn't a big fan...
There is a bit of category theory applied to programming in https://github.com/affeldt-aist/monae.
Barr and Wells is IMHO very very good [and free] http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf
Thanks will have a look
@vlj maybe Seven sketches in compositionality
Not specific about computer science, but it looks like it is presenting quite nicely the important categorical ideas rather than emphasizing on the technicalities.
This topic was moved here from #Coq users > Learning category theory as a programmer by Théo Zimmermann
We use Steve Awodey's book for the master students here at Aarhus university. It's quite accessible.
There's also a very active category zulip server, where they have entire topics devoted to discussing better introductions for different backgrounds :)
https://categorytheory.zulipchat.com/
@Alexander Gryzlov it looks like you need an invitation to join this zulip server (I just tried to join)
I have some trouble having the intuition on homset and the set categories. It looks like every categories can be "plunged" inset, there is even the forgetful functor for this. But for instance a monoid seen as a category is a single node and arrows for every element, but it looks like the nature of this node can be arbitrary. One can map the node to the set of all elements of the node to make it set like but it looks like artificially setting a set to something that's basically "nothing special". Same for the graph category, category theory talks about set of node, but itassumes that the node can be part of the set.
And about homsets, they are element of set if I understand correctly, but is it always safe to assume this ? I mean there are small categories and big categories to avoid self referential sets inconsistencies so I would expect that putting homset in set is only possible for some categories but not all possibles one.
Homsets are of course sets, but there are categories for which the homset is not a set, but rather a category
@vlj if you’re familiar with universes in Coq, and with how you have Type@{0} : Type@{1} : Type@{2} : ..., then IIUC you can think of “small” and “big” as “in Type@{0}“ and “in Type@{1}”.
so for large categories, homsets are basically still sets, but instead of being in the Type@{0} universe, they’re in the next universe, Type@{1}.
and you can consider even larger categories in Type@{2}, etc.
(even tho Coq normally hides all that)
(I am not being very precise here, and I haven’t studied a proper treatment of this stuff — “small” and “large” are usually talking about set theory, but you can also set up universes there, if you are willing to use the analogue of Coq’s universe hierarchy — that is,suitable inaccessible cardinals, or in particular Grothendieck universes)
I am a mathematical dumb dumb, so the resources I've used to try and understand some category theory are for mathematical dumbs dumbs. They may be too basic for you, but I liked them
This book was pretty introductory, but goes into a lot of great detail that is quite lacking in a lot of the stuff on category theory intended for mathematicians. Very well written
https://www.amazon.com/Conceptual-Mathematics-First-Introduction-Categories/dp/052171916X
This is a bit more advanced than the previous, but I found it very well written and it helped me understand things that I didn't really grok from other sources
https://www.amazon.com/Category-Cambridge-Studies-Advanced-Mathematics/dp/1107044243
This book covers a ton of ground. It's good if your goal is to understand the language, and understand things like the Yoneda Lemma, but it won't go too much deeper...mainly it sort of just lays out what is going on in Category theory with some proofs, but definitely not the rigor of something like Awodey's book
https://github.com/hmemcpy/milewski-ctfp-pdf
I think the next step after all that would probably be Awodey's book. I picked it up once, decided that given my current mathematical sophisticated and level of need it was a bit too hard, then put it down. -_-
I've also read Benjamin Pierce's book, and it is good, but it covers stuff subsumed by the above and I think they do it better (with all respect due to the brilliant Dr Pierce!)
@vlj I think there is a small (but rather technical) mistunderstanding. Not all categories can be embedded into Set: there is of course a size issue but that can be "solved" up to some point by considering universes of various sizes, but more fundamentally there are categories that just don't embed into set because they are too different (as explained in this paper by Peter Freyd -- not necessarily an easy read). A category that can be embedded into Set is usually said to be concrete, and there are various theorems ensuring that categories built out of Set (such as categories of algebras for a theory or a monad) are concrete.
If a category is not concrete then homset are still in set ?
yes with the standard definition of a category. Things get different once you start talking about enriched and/or higher categories.
Kenji Maillard said:
yes with the standard definition of a category. Things get different once you start talking about enriched and/or higher categories.
Actually I believe that depends a lot on the reference definition you take. In some cases, these are rather called locally small categories.
right, but if a category isn’t locally small, the homsets are still “collections”, just too large to be sets; in ZFC they are classes, but with a hierarchy of universes, homsets of larger categories are members of bigger universes.
And I also recall, like @Cyril Cohen, that some texts assume all categories to be locally small.
Is there a good book/article presenting the Lawvere category for beginner ? It looks like a very important part of category theory but the barr well ebook doen't present it (it just mention Lawvere various papers)
@vlj this is not really tailored for programmers / CS but may help https://www.irif.fr/~mellies/mpri/mpri-ens/articles/hyland-power-lawvere-theories-and-monads.pdf
thanks
Is there a tool/Javascript lib that can be used to create small animations of arrows/points ? I find it easier to explain things in category theory with step by step drawing, and I wonder if there is a tool that allows to create animated diagram quickly
Is there a good pdf/book to introduce infinity catégories ?
Higher Topos Theory by Jacob Lurie maybe ? For a quick glance at what the theory looks like these notes (in french) by Denis-Charles Cisinski might help. And for the model independent approach, there is this ongoing work by Emily Riehl and Dominic Verity.
thanks !
I don't know if it's relevant for programming, but I'd like to have at list a clue at what is generalised
I read that dépendent types can be viewed as fibration but I have troubles making the connections.
Afaik a fibration is a functor P from C to D which has cartesian arrows for f in D and point x in C with P(x) = dst(f).
If I have a dépendent type forall x:A, B(x) then I'm not sure if B should be viewed as C or D in the fibration definition.
Intuitively I would say that B is C since there are several objets that can be projected to a single x in C.
But I tend to see functor moving things "above" source category (maybe I have thé wrong picture here) and the traditionnal picture is that the dépendant types lie over the indexing type
Hi @vlj, I think you can understand the claim "dependent types can be viewed as fibrations" along the following line: there exists models of dependent type theory where types are interpreted as objects with some structure and type families as -fibrations. I think one of the simplest example is to take to be groupoids (see this seminal paper), but that also apply to simplicial sets, and at least some variants of cubical sets (of course in each case the precise definition of "fibration" vary).
So the short answer is that correspond to the base of the "fibration" and to the functor .
Now, you were trying to view as a Grothendieck fibration, interpreting types as categories. To my knowledge such an interpretation has never been put on paper formally. The closest thing are problably the ongoing work on directed type theory (for instance Thorsten Altenkrich's slides or Andreas Nuyts's master thesis).
Thanks for the references and explanation
By the way does the HoTT book assume such interpretation of type as categories ? At least in the chapter 2 they mention the word "fibration" to talk about dependant type iirc, but they assume no prior knowledge of category theory and redefine things like horizontal composition and whiskering without mentionning natural transformation, so actually they don't mention any category at all
is there a more general concept of fibration than the one found in category theory ?
@Kenji Maillard If one of the simplest S is groupoids, what’s wrong with taking S to be the category of sets
@vlj There is a _less general_ concept of fibration, which comes before the CT one:
Topologically, the transportation lemma can be viewed as a “path lifting” operation in a fibration.
In classical homotopy theory, a fibration is defined as a map for which there exist liftings of paths; while in contrast, we have just shown that in type theory, every type family comes with a specified “path-lifting function”.
Those sentences hint that the relevant field is “topology” or “homotopy theory”
@vlj To me, the basic answer is that to view x : A |- B
as a fibration, intuitively, you need to think of Sigma x : A. B
and of its projections
the first projection identifies the fiber, the second produces a point in that fiber
vlj said:
is there a more general concept of fibration than the one found in category theory ?
One thing I forgot to mention is that the word fibration is employed a lot in algebraic topology as explained by @Paolo Giarrusso , and that abstracting/categorifying it lead in particular to the notion of model category where fibrations are part of the structure (they are a class of maps satisfying some lifting properties).
Paolo Giarrusso said:
Kenji Maillard If one of the simplest S is groupoids, what’s wrong with taking S to be the category of sets
Nothing is wrong, but I find it weird to insist on the word "fibration" when it's just a plain map between sets without additional data or structure :)
well, it’s useful to instantiate those generic frameworks for models onto Set, to get models in the category of sets.
however, what model is most interesting/appropriate depends on the audience, and I can’t tell if @vlj is a mathematician or a computer scientist ^H^H^H what their goal is
(IMHO, the model in sets is appropriate for most programmers — except that when you want to understand HoTT, there you indeed need _at least_ groupoids)
but to be clear, I’m only a beginner in this material and Kenji understands much more than me; I only contributed to say a few more words on the basics ;-)
thanks for the precision
Last updated: Jun 01 2023 at 13:01 UTC