nLab essentially algebraic theory



Higher algebra

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




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 C 0C_0 of objects, a set C 1C_1 of morphisms, source and target maps s,t:C 1C 0s,t : C_1 \to C_0 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:


An essentially algebraic theory or finite limits theory is a category that is finitely complete, i.e., has all finite limits. A model of an essentially algebraic theory TT is a functor

F:TSetF: T \to Set

that is left exact, i.e., preserves all finite limits. A homomorphism of models is a natural transformation

α:FF \alpha : F \to F'

between left exact functors F,F:TSetF, F' : T \to Set. Models of an essentially algebraic theory TT and the homomorphisms between them form a category Mod(T)=Lex(T,Set)Mod(T) = Lex(T, Set).

More generally, for any category with finite limits XX, we can define the category of models of TT in XX, Lex(T,X)Lex(T, X), which has left exact functors F:TXF: T \to X 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 a finitary essentially algebraic theory. We do this in what follows.

A more traditional syntactic definition (following Adámek–Rosicky; see the references below) is as follows:


An essentially algebraic theory is a quadruple

Γ=(Σ,E,Σ t,Def)\Gamma = (\Sigma, E, \Sigma_t, Def)

where Σ\Sigma is a many-sorted signature consisting only of operation symbols, EE is a set of Σ\Sigma-equations, Σ tΣ\Sigma_t \subseteq \Sigma is a set of operation symbols called “total”, and DefDef is a function which assigns, to each operation σΣΣ t\sigma \in \Sigma - \Sigma_t of type iIs is\prod_{i \in I} s_i \to s, a set Def(σ)Def(\sigma) of Σ t\Sigma_t-equations involving only variables x iVar(s i)x_i \in Var(s_i).

A (set-theoretic) model MM of a theory Γ\Gamma assigns to each sort ss a set M(s)M(s), to each operation symbol σ: iIs is\sigma: \prod_{i \in I} s_i \to s of Σ\Sigma a partial function

M(σ): iIM(s i)M(s)M(\sigma): \prod_{i \in I} M(s_i) \to M(s)

such that

  • For each σΣ t\sigma \in \Sigma_t the function M(σ)M(\sigma) is a total function;

  • For each σΣΣ t\sigma \in \Sigma - \Sigma_t of type iIs is\prod_{i \in I} s_i \to s, and each II-tuple

    a=a i iI iIM(s i),a = \langle a_i \rangle_{i \in I} \in \prod_{i \in I} M(s_i),

    M(σ)(a)M(\sigma)(a) is defined if and only if all the equations in Def(σ)Def(\sigma) are satisfied at the argument aa.

  • All the equations of EE are satisfied (i.e. the restrictions of both partial functions to the intersection of their domains of definitions are equal).

Homomorphisms of models θ:MM\theta: M \to M' are defined in the standard way: a collection of functions θ(s):M(s)M(s)\theta(s): M(s) \to M'(s) for each sort of the signature Σ\Sigma which are compatible with the M(σ),M(σ)M(\sigma), M'(\sigma) 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 duality between essentially algebraic theories and their categories of models is given by Gabriel-Ulmer duality.


  • A (multisorted) Lawvere theory TT is the same thing (has the same models) as a finitary essentially algebraic theory in which all operations are total. If C TC_T is the opposite of the category of finitely presented TT-algebras, then the category of models is equivalent to Lex(C T,Set)Lex(C_T, Set).

  • 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, CatCat is not the category of models of any equational Horn theory, nor is even the category PosPos of posets. See this paper by Barr for a proof. Essentially algebraic theories are equivalent to partial Horn theories (Palmgren, Vickers).

  • An equivalent formulation is as a cartesian theory, a geometric theory in which disjunction \bigvee is not used, and each use of existential quantification \exists must be accompanied by a proof that existence is unique. See Elephant.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus


Freyd first introduced essentially algebraic theories here:

A nice equivalent formulation can be found in

Cartesian theories were introduced under different names in the early seventies by John Isbell, Peter Freyd and Michel Coste (cf. Johnstone 1979). A standard source is Johnstone (2002).

  • Peter Freyd, Cartesian Logic , Theor. Comp. Sci. 278 (2002) pp.3-21.

  • Peter Johnstone, A Syntactic Approach to Diers’ Localizable Categories , pp.466-478 in Springer LNM 753 Heidelberg 1979.

  • Peter Johnstone, Sketches of an Elephant II , Oxford UP 2002. (Around D1.3.4 p.833)

A short introductory/overview note:

  • Andreas Nuyts, Understanding Universal Algebra Using Kleisli-Eilenberg-Moore-Lawvere Diagrams, note

Last revised on March 12, 2024 at 15:07:29. See the history of this page for a list of all contributions to it.