Dependent type theory and higher algebraic structures

Abstract: In classical universal algebra, every family of algebraic structures (such as monoids, groups, rings, modules, small categories, operads, sheaves) can be classified by a syntactic (algebraic or essentially algebraic) equational theory. A cornerstone of universal algebra is the equivalence between algebraic theories and finitary monads on the category of sets, due to Lawvere, B\'enabou and Linton. Higher algebraic structures (such as loop spaces, E-k spaces, infinity-categories, infinity-operads and their modules and algebras, stacks, spectra) are algebraic structures up to homotopy in spaces ("spaces" = topological spaces, simplicial sets or any other model of homotopy types). It is a long-standing presupposition among homotopy type theorists that the dependent types introduced by Martin-L\"of are particularly well-suited to providing syntactic theories and a universal algebra for higher algebraic structures. In this talk, we will see a (few) definition(s) of "dependently sorted/typed algebraic theory" and describe a monad-theory equivalence strictly generalising that of Lawvere-Bénabou-Linton. With respect to their Set-valued models, dependently sorted algebraic theories have the same expressive power as essentially algebraic theories. However, as we will see in this talk, dependently sorted algebraic theories have the advantage of having a good theory of models up-to-homotopy in spaces, which generalises the theory of homotopy-models of algebraic theories due to Schwede, Badzioch, Rezk and Bergner. We will see that many familiar algebraic structures (such as n-categories, omega-categories, coloured planar operads, opetopic sets) are very naturally seen to be models of dependently sorted algebraic theories. The crux of these results is a correspondence between the dependent sorts/types of any dependently sorted algebraic theory T, and a certain "cellularity" underlying every algebraic structure described by T (i.e. every T-model). The goal of this talk will be to explain this correspondence between type dependency and cellularity, and why this cellularity marries well with homotopy theory.

machine learningcommutative algebraalgebraic geometryalgebraic topologycombinatoricscategory theoryoperator algebrasrings and algebrasrepresentation theory

Audience: researchers in the topic

( chat )

Algebraic and Combinatorial Perspectives in the Mathematical Sciences

Series comments: To receive announcements: Register into our mailing list by going to our main website www.math.ntnu.no/acpms/