[Berkeley Seminar] CB Aberle: All Concepts are Essentially Algebraic

Title: All Concepts are Essentially Algebraic
Abstract: Lawvere's categorical formulation of algebraic theories enables one to study some of the most common structures found in mathematics – e.g. groups, rings, etc. – at a high level of precision and generality. However, many significant mathematical concepts, including categories, topological spaces, etc., turn out not to be algebraic, in this sense. Notably, the very framework used by Lawvere to describe algebraic theories and their models – categories with finite products and product-preserving functors between them – cannot be described as an algebraic theory, and so it seems that algebra alone cannot encompass the whole of mathematics (nor even itself). There is, however, a deeper sense in which all of mathematics is essentially algebraic. What is needed to reveal this fact is to adapt the classical notion of algebraic theories, which are fundamentally simply typed, to an appropriate notion of dependently typed algebraic theories. At this level of generality, one is capable of defining not only individual mathematical structures, but structures that themselves encompass whole universes of mathematics, including topoi, models of type theory, etc. In particular, the theory of dependently-typed algebraic theories is itself describable as a dependently-typed algebraic theory. This fact has many profound consequences, of which I shall highlight just one: using the framework of dependently-typed algebraic theories, one can construct a type theory whose types themselves correspond to type theories, with functions between these types corresponding to translations between the corresponding type theories.

[cbaberle]

Oh hey, that's me! One quick correction to something I said in the talk: if you view the theory of elementary topoi equipped with a topological space as a category fibred over (the category given by the theory of) elementary topoi, the fibre of the topos Set isn't quite the usual category of topological spaces and continuous maps – instead, it's the category of topological spaces and *open* maps. So you need to do a little more work to get out the category of topological spaces and continuous maps, although it is still possible. This is closely related to Owen's point later in the talk about getting the 2-category of topoi and geometric morphisms out of this sort of setup (inasmuch as geometric morphisms are the topos-theoretic analogue of continuous maps).

[akompsupport]

The transcript provided is a conversation between David Berlekamp, Michael Francis and Daniel Calegari discussing the concepts of algebraic theories in type theory for mathematics.

1) **David** starts by introducing an analogy with categories to explain why they are important. He says that categorical structures like topologies (where points can be assigned types from a set T into another category S, typically called SetCat or TopoCats), and finite limits of these cat subcategories under filtered colimits in CSubs make up the mathematical language for algebraic theories.

2) **David** then introduces "types" as an abstraction that captures essential properties like identity types (a pair with two elements: one being equal to another). The type theory he describes is very much dependent on context, allowing structures and formulas only valid within specific contexts. This distinction between pure syntax vs semantics helps clarify the limitations of algebraic theories.

3) **David** explains how these categories can be constructed using a technique called "conversion" from category notation (where objects are labeled with types in one direction followed by morphisms that relate those two labels and so forth, similar to ordinary programming languages like Java or Python)) into type-theoretical context-sensitive language.

4) **David** uses an example of the CategoryTheory toolbox for TypeScript's syntax tree representation as a way how he constructs categories. He also mentions some advanced features such "recursive pattern matching" and basic functionalities, all within this specific setting to demonstrate its applicability in constructing category-like structures out-of-the-box.

5) **David** closes by comparing the type theory of algebraic theories with other formal languages that use types but differ significantly: he discusses how TypeScript's syntax can be interpreted as a framework for dependent typed functional programming, which includes terms and substitutions within contexts. He concludes his talk saying there is more work to do on this topic.

6) **Michael** comments about the simplicity of algebraic theories in general (a single type theory with no arbitrary structure at all), but emphasizes that categorical structures like TopoCats are quite useful when one wants a formal framework for mathematics or computer science. He also refers back briefly to David's analogy between categories and topologies, showing how mathematical concepts can be naturally encoded using category-theoretic language.

The conversation is rich with examples of type theory constructs (types as abstract sets/morphisms in certain context) being used within this particular setting like constructing the CategoryCats toolbox or interpreting a TypeScript syntax tree. The discussion touches on various aspects such linguistic nuances, mathematical properties and how these concepts can be formalized using programming languages that encapsulate type theory.

Overall it demonstrates why category-theoretic language has found its place in modern mathematics as an expressive yet powerful system for describing abstract structures like topologies or algebra models.

[funktorial]

hey nice talk! one way to view the failure of topological spaces to be algebraic is as a problem of variance: the *opposite* of the category of topological spaces is a quasivariety, and thus locally finitely presentable

[infinidimensionalinfinitie]

all concepts are essentially non-mathematical;
as much as they are mathematical;