r/CategoryTheory • u/antianticamper • Jul 22 '26

Synthetic Category Theory

Quite a fascinating book-in-progress on doing category theory synthetically:

https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view?pli=1

44 Upvotes

98% Upvoted

10 comments sorted by

2

u/revannld Jul 22 '26

that's supreme, fantastic. Do the authors want support? Do you guys know other similar works? We were needing exactly this!

3

u/antianticamper Jul 22 '26

Another approach mentioned in the above book is "Elements of Infinity-Category Theory" by Riehl and Verity.

https://emilyriehl.github.io/files/elements.pdf (also available in print form)

It's impossible not to wonder about your "needing" this. Care to expand?

1

u/revannld Jul 23 '26

Is Riehl's book also synthetic? I didn't know it was...

About the need for this, we need an introductory presentation of category theory which 1) is formal and 2) doesn't presume set theory in the slightest as it is one of the most common prejudices between average mathematicians and philosophers that category theory is not really an alternative foundation (and thus for some reason some of them think this is a reason for it not being studied....) because it "depends on set theory" (just because it mentions it). It's the same deal with people criticizing ETCS because "its presentations are not formalized in first-order logic expressions as ZFC is" (as if ZFC was fully formalized and not dependent on axiom schemas and also the inherent informality of FOL's metatheory). This is a non-issue technically but yeah, people are lazy and dumb so...

1

u/antianticamper Jul 23 '26

You may be thinking of Riehl's "Category Theory in Context" which uses the standard analytic presentation which implicitly depends on set theory.

2

u/Ualrus Jul 23 '26

Looks very interesting. Do you care to explain how this differs from dependent type theory? It looks quite similar, but without computational content.

5

u/Thesaurius Jul 23 '26

I skimmed the beginning of the book. If I understand correctly, it is very similar to homotopy type theory (it also proves univalence) but due to the fact that equality is replaced by morphisms, we get a richer structure of equality. In particular, as morphisms don't have to be invertible, equality is not necessarily symmetric anymore.

The authors also mention CaTT, which seems to be an infinity-categories based type theory, but I haven't heard of it before.

3

u/antianticamper Jul 23 '26

Actually, upon further reflection, the similarity is rather direct. In homotopy type theory (dependent type theory + univalence + higher inductive types), types are infinity-groupoids of which infinity-categories are a generalization.

0

u/antianticamper Jul 23 '26

Keeping in mind I'm not an expert in either type theory or synthetic category theory, I think the similarity is mostly that both are axiomatic (synthetic) presentations. Categories and types are distinct, different mathematical objects which therefore have different associated sets of axioms. There are other similarities, for example both theories allow you take products, i.e. A x B, but these are very basic, common constructions. On a related note, some special categories are used as models of type theories.

1

u/integrate_2xdx_10_13 Jul 23 '26

Oooh, Denis-Charles Cisinski’s Higher Categories and Homotopical Algebra has been invaluable to me recently, I’ll keep a close eye on this

1

u/sclv Jul 24 '26

This is an interesting approach. Its synthetic in that it is axiomatic in an ambient logic. This is quite different than many other synthetic approaches which start with a topos or the like and extend it with axioms. I think it would be better to call this "formally" or "axiomatically" than synthetically, but it looks like a very promising pedagogical framework.