# Categorial foundations via "categories of algebras"

There are categorical foundations for mathematics axiomatizing the category of sets (Lawvere's ETCS), cartesian closed categories (type theory), and the category of spaces (homotopy type theory). Categories in foundations commonly have properties such as distributivity of products over coproducts, extensivity, or cartesian closed-ness, making them vaguely space-like.

We also know from studies of Isbell duality that categories of algebras and categories of spaces sit in a kind of duality with each other. Moreover, categories of algebras are commomly codistributive and coextensive (e.g. $$R$$-algebras). While they are not always co-cartesian co-closed, this is perhaps analogous to how one must consider the cocompletion $$[C^{op}, \text{Set}]$$ of a category $$C$$ to fill in the missing objects and gain the desired cartesian closed property.

Question: What is a "foundational category of algebras" much like Set is the "foundational category of spaces"?

My question is partially motivated by a interest in asymmetry underlying mathematics. If categories sit in a sort of duality in the sense Isbell and Lawvere exposed, why is one side of this duality preferable for foundations?

To elaborate, if an ‘abstract set’ is intuitively one whose elements lack internal structure (operations, cohesion, etc.), we may wish to do the same, but instead axiomatize "function spaces with the least amount of internal structure".

Analogizing, we might expect this category to behave as follows:

1) I would expect interesting categories of space to be comonadic over a candidate for this "category of algebras".

2) $$\text{Set}$$ is devoid of cohesion. The analogous situation for "categories of algebras" would mean that $$\text{Alg}$$ (I guess that's what would call this category) is internally devoid of "co-cohesion".

3) Categories of cosheaves inside $$[C^{op}, \text{Alg}]$$ would make further categories of algebras, just as categories of sheaves on $$[C^{op}, \text{Set}]$$ make further categories of sheaves. (lawvere theories are like certain kinds of cosheaves).

4) I wonder about the category of heyting algebras as a candidate. Heyting algebras arise as algebras of subobjects of a topos, so that $$[X, \Omega ]_{T}$$ is a Heyting algebra for a topos $$T$$ with subobject classifier $$\Omega$$.

• You're like, asking how to put together the last 60 years of research in category theory :) Feb 1 '20 at 21:33
• @Fosco :) That makes me think, my question is easily too much to ask for a mathoverflow question. I should instead say that I am content with guesses and references to where people have elsewhere considered the question of asymmetry in category theory. Feb 2 '20 at 0:40
• I'm sure you know that $\mathbf{Set}^{op} \simeq \mathbf{CABA}$ (nLab link), is this the sort of thing you were thinking, for $\mathbf{Set}$? Feb 2 '20 at 0:53
• Interesting and nice question! But the first sentence is a bit misleading — when you say there are foundations “axiomatizing sets (Lawvere's ETCS), cartesian closed categories (type theory), and spaces (homotopy type theory)”, the middle part of the analogy doesn’t match up. Sets in ETCS and spaces in HoTT are not analogous to CCC’s in simple type theory, but to the objects of the CCC. To make the analogy fit better, one could say simple type theory is axiomatising a more primitive/general/weaker sense of sets, or (more concisely) that it’s axiomatising datatypes. Feb 2 '20 at 15:51
• @PeterLeFanuLumsdaine I see what you mean- I made some edits adjusting for your concerns. Let me know if it fixes it. Feb 4 '20 at 1:02