essentially algebraic theories

[Vladimir Voevodsky]

Hello,

what would be a good reference for the definition of what an essentially algebraic theory is?

Vladimir.

[Steve Awodey]

Freyd, P.: "Aspects of Topoi", Bull. Austr. Math. Soc. 7, pp. 1--76, 467--80.

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Steve Awodey]

it’s 1972.

here’s a link:

http://ncatlab.org/spahn/files/aspects_of_topoi.pdf

[Andrej Bauer]

For a quick description there is the nlab page:
http://ncatlab.org/nlab/show/essentially+algebraic+theory

Otherwise, I think it can be found in:

J. Adámek, M. Hébert, J. Rosický: "On essentially algebraic
theorries and their generalizations",
Algebra Universalis, August 1999, Volume 41, Issue 3, pp 213-227
http://link.springer.com/article/10.1007/s000120050111

but my home connection doesn't allow me to double-check.

With kind regards,

Andrej

[Andrej Bauer]

Actually, a better source might be Section 3.D of

Locally Presentable and Accessible Categories
Jiří Adámek, J. Rosicky
Cambridge University Press, 1994
http://books.google.si/books?id=iXh6rOd7of0C

With kind regards,

Andrej

[Vladimir Voevodsky]

Where can one find a definition of a “partially algebraic theory”?

[Bas Spitters]

You might also find this useful:
Palmgren and Vickers
Partial Horn logic and cartesian categories
http://www.sciencedirect.com/science/article/pii/S0168007206001229
---
A logic is developed in which function symbols are allowed to
represent partial functions. It has the usual rules of logic (in the
form of a sequent calculus) except that the substitution rule has to
be modified. It is developed here in its minimal form, with equality
and conjunction, as “partial Horn logic”.

Various kinds of logical theory are equivalent: partial Horn theories,
“quasi-equational” theories (partial Horn theories without predicate
symbols), cartesian theories and essentially algebraic theories.

The logic is sound and complete with respect to models in Set, and
sound with respect to models in any cartesian (finite limit) category.

The simplicity of the quasi-equational form allows an easy predicative
constructive proof of the free partial model theorem for cartesian
theories: that if a theory morphism is given from one cartesian theory
to another, then the forgetful (reduct) functor from one model
category to the other has a left adjoint.

Various examples of quasi-equational theory are studied, including
those of cartesian categories and of other classes of categories. For
each quasi-equational theory TT another, CartϖT, is constructed, whose
models are cartesian categories equipped with models of TT. Its
initial model, the “classifying category” for TT, has properties
similar to those of the syntactic category, but more precise with
respect to strict cartesian functors.
---

[Vladimir Voevodsky]

Interesting. So they suggest to consider only operations of rank 0 (everywhere defined) and rank 1 (domain of definition is given by equations between operations of rank 0) (terminology is mine, V.V.)

This can be done at the cost of increasing the number of sorts. For example if one wants to define the condition that a square is a pull-back square as an essentially algebraic condition, one needs to use an operation that is defined on pairs of morphisms with a certain condition on the compositions of these morphisms with the given morphisms - i.e. an operation that is defined on the subsets that are given by equations that involve operations of rank 1 (compositions).

Instead one can introduce a new sort for composable pairs of morphisms and a number of new operations but they will all be of rank <= 1.

I think in many cases a more general notion where operations of all ranks are permitted is useful.

Vladimir.

[Michael Shulman]

On Fri, Feb 13, 2015 at 11:40 AM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I think in many cases a more general notion where operations of all ranks are permitted is useful.

I believe one place such a definition can be found is under the name
"cartesian theory" in D1.3.4 of "Sketches of an Elephant".