symmetric monoidal (∞,1)-category of spectra
|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
A mathematical structure is essentially algebraic if its definition involves partially defined operations satisfying equational laws, where the domain of any given operation is a subset where various other operations happen to be equal. An actual algebraic theory is one where all operations are total functions.
The most familiar example may be the (strict) notion of category: a small category consists of a set of objects, a set of morphisms, source and target maps and so on, but composition is only defined for pairs of morphisms where the source of one happens to equal the target of the other.
Essentially algebraic theories can be understood through category theory at least when they are finitary, so that all operations have only finitely many arguments. This gives a generalisation of Lawvere theories, which describe finitary algebraic theories.
As the domains of the operations are given by the solutions to equations, they may be understood using the notion of equalizer. So, just as a Lawvere theory is defined using a category with finite products, a finitary essentially algebraic theory is defined using a category with finite limits — or in other words, finite products and also equalizers (from which all other finite limits, including pullbacks, may be derived).
As alluded to above, the most concise and elegant definition is through category theory. The traditional definition is this:
that is left exact, i.e., preserves all finite limits. A homomorphism of models is a natural transformation
between left exact functors . Models of an essentially algebraic theory and the homomorphisms between them form a category .
More generally, for any category with finite limits , we can define the category of models of in , , which has left exact functors as objects and natural transformations between these as morphisms.
However, the finiteness restriction on the limits above is not part of the core concept of an ‘essentially algebraic’ structure, so one may prefer to call a category with finite limits an finitary essentially algebraic theory. We do this in what follows.
A more traditional syntactic definition (following Adamek–Rosicky; see the references below) is as follows:
An essentially algebraic theory is a quadruple
where is a many-sorted signature consisting only of operation symbols, is a set of -equations, is a set of operation symbols called “total”, and is a function which assigns, to each operation of type , a set of -equations involving only variables .
A (set-theoretic) model of a theory assigns to each sort a set , to each operation symbol of a partial function
For each the function is a total function;
For each of type , and each -tuple
is defined if and only if all the equations in are satisfied at the argument .
All the equations of are satisfied (i.e., are interpreted as equations between partial functions).
Homomorphisms of models are defined in the standard way: a collection of functions for each sort of the signature which are compatible with the in the evident way.
The point is that (in the finitary case) either notion of theory may be used to specify the same category of models, and that
Categories of models of finitary essentially algebraic theories are precisely equivalent to locally finitely presentable categories. These are equivalent to categories of models of finite limit sketches.
A (multisorted) Lawvere theory is the same thing (has the same models) as a finitary essentially algebraic theory in which all operations are total. If is the opposite of the category of finitely presented -algebras, then the category of models is equivalent to .
As mentioned above, categories are models of a finitary essentially algebraic theory.
An equational Horn theory is essentially algebraic, but not all essentially algebraic theories are equational Horn theories. Perhaps surprisingly, is not the category of models of any equational Horn theory, nor is even the category of posets. See this paper by Barr for a proof.