Skip to main content
MathOverflow

Return to Question

added 151 characters in body
Source Link
antoine_vm
antoine_vm
  • 121
  • 4

I am a newcomer to universal algebra and I just read this (very good, IMO) book on the topic:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

The authors most notably treat the case of 1-sorted first-order finitary Lawvere theories (equivalently: finitary monads). This is, as I understand it, the most common level of generality appearing in the literature to deal with (categorical) universal algebra.

Additionally the authors explain the relation between "old-fashioned" universal algebra -- which we'll call equational theories here -- and Lawvere theories, as well as the relation between Lawvere theories and categories of models of Lawvere theories. The quick and informal upshot is that there is a pair of such adjunctions: old universal algebra, lawvere thies, models Where $\mathrm{EqTh}$ is the category of equational theories (that is: signatures + equations), $\mathrm{AlgTh}$ is the category of Lawvere theories, $\mathrm{AlgCat}$ is the category of algebraic categories. Algebraic categories are basically defined to be categories of models of Lawvere theories. The first adjunction connects particular presentations of theories to Lawvere theories. The second adjunction is some kind of Gabriel-Ulmer duality and links theories to their models.

My questions is: what are the existing ways we can generalize this picture? And is there an ultimate framework encompassing all those generalizations? For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Some examples of generalisations (either on the presentation side or on the Lawvere theory side or on both sides): higher-order logic, enriched Lawvere theories, sketches, Makkai's first order logic dependent sorts (FOLDS), infinitary theories. I'm sure there are a lot more!

EDIT: Here is a paper about higher order algebraic theories

I am a newcomer to universal algebra and I just read this (very good, IMO) book on the topic:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

The authors most notably treat the case of 1-sorted first-order finitary Lawvere theories (equivalently: finitary monads). This is, as I understand it, the most common level of generality appearing in the literature to deal with (categorical) universal algebra.

Additionally the authors explain the relation between "old-fashioned" universal algebra -- which we'll call equational theories here -- and Lawvere theories, as well as the relation between Lawvere theories and categories of models of Lawvere theories. The quick and informal upshot is that there is a pair of such adjunctions: old universal algebra, lawvere thies, models Where $\mathrm{EqTh}$ is the category of equational theories (that is: signatures + equations), $\mathrm{AlgTh}$ is the category of Lawvere theories, $\mathrm{AlgCat}$ is the category of algebraic categories. Algebraic categories are basically defined to be categories of models of Lawvere theories. The first adjunction connects particular presentations of theories to Lawvere theories. The second adjunction is some kind of Gabriel-Ulmer duality and links theories to their models.

My questions is: what are the existing ways we can generalize this picture? And is there an ultimate framework encompassing all those generalizations? For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Some examples of generalisations (either on the presentation side or on the Lawvere theory side or on both sides): higher-order logic, enriched Lawvere theories, sketches, Makkai's first order logic dependent sorts (FOLDS), infinitary theories. I'm sure there are a lot more!

I am a newcomer to universal algebra and I just read this (very good, IMO) book on the topic:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

The authors most notably treat the case of 1-sorted first-order finitary Lawvere theories (equivalently: finitary monads). This is, as I understand it, the most common level of generality appearing in the literature to deal with (categorical) universal algebra.

Additionally the authors explain the relation between "old-fashioned" universal algebra -- which we'll call equational theories here -- and Lawvere theories, as well as the relation between Lawvere theories and categories of models of Lawvere theories. The quick and informal upshot is that there is a pair of such adjunctions: old universal algebra, lawvere thies, models Where $\mathrm{EqTh}$ is the category of equational theories (that is: signatures + equations), $\mathrm{AlgTh}$ is the category of Lawvere theories, $\mathrm{AlgCat}$ is the category of algebraic categories. Algebraic categories are basically defined to be categories of models of Lawvere theories. The first adjunction connects particular presentations of theories to Lawvere theories. The second adjunction is some kind of Gabriel-Ulmer duality and links theories to their models.

My questions is: what are the existing ways we can generalize this picture? And is there an ultimate framework encompassing all those generalizations? For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Some examples of generalisations (either on the presentation side or on the Lawvere theory side or on both sides): higher-order logic, enriched Lawvere theories, sketches, Makkai's first order logic dependent sorts (FOLDS), infinitary theories. I'm sure there are a lot more!

EDIT: Here is a paper about higher order algebraic theories

Became Hot Network Question
Source Link
antoine_vm
antoine_vm
  • 121
  • 4

Comparing the existing formulations of universal algebra and their levels of generality

I am a newcomer to universal algebra and I just read this (very good, IMO) book on the topic:

Adámek, J., Rosický, J., & Vitale, E. M. (2010). Algebraic theories: a categorical introduction to general algebra (Vol. 184). Cambridge University Press.

The authors most notably treat the case of 1-sorted first-order finitary Lawvere theories (equivalently: finitary monads). This is, as I understand it, the most common level of generality appearing in the literature to deal with (categorical) universal algebra.

Additionally the authors explain the relation between "old-fashioned" universal algebra -- which we'll call equational theories here -- and Lawvere theories, as well as the relation between Lawvere theories and categories of models of Lawvere theories. The quick and informal upshot is that there is a pair of such adjunctions: old universal algebra, lawvere thies, models Where $\mathrm{EqTh}$ is the category of equational theories (that is: signatures + equations), $\mathrm{AlgTh}$ is the category of Lawvere theories, $\mathrm{AlgCat}$ is the category of algebraic categories. Algebraic categories are basically defined to be categories of models of Lawvere theories. The first adjunction connects particular presentations of theories to Lawvere theories. The second adjunction is some kind of Gabriel-Ulmer duality and links theories to their models.

My questions is: what are the existing ways we can generalize this picture? And is there an ultimate framework encompassing all those generalizations? For instance I would be interested to hear about what can be done to obtain type theories as some kind algebraic theories.

Some examples of generalisations (either on the presentation side or on the Lawvere theory side or on both sides): higher-order logic, enriched Lawvere theories, sketches, Makkai's first order logic dependent sorts (FOLDS), infinitary theories. I'm sure there are a lot more!