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 $A$ are interpreted as objects with some structure $\mathcal{S}$ and type families $x : A \vdash B$ as $\mathcal{S}$-fibrations. I think one of the simplest example is to take $\mathcal{S}$ 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 $A$ correspond to the base of the "fibration" $D$ and $B$ to the functor $P : C \Rightarrow D$.

Now, you were trying to view $B$ 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: Sep 28 2023 at 11:01 UTC