nLab structure


This entry is about a general concepts of “mathematical structure” such as formalized by category theory and/or dependent type theory. This subsumes but is more general than the concept of structure in model theory.






It is common in informal language to speak of mathematical objects “equipped with extra structure” of some sort. The archetypical examples are algebras over a Lawvere theory in Set: these are sets equipped with the structure of certain algebraic operations. For instance a group (G,e,)(G, e, {\cdot}) is a set GG equipped with a binary operation :G×GG{\cdot} : G \times G \to G, etc.

One may formalize the notion of structure using the language of category theory. This is discussed at stuff, structure, property. In that formalization objects in some category DD are objects in some category CC equipped with extra structure if there is a functor p:DCp \colon D \to C such that

Depending on author and situation, more properties are required of this functor (Ehresmann 57, Ehresmann 65, Adamek-Rosicky-Vitale 09, remark 13.18):

However, notice that these two conditions violate the principle of equivalence for categories. In the terminology of strict categories one might hence refer to these conditions as expressing “strict extra structure”.

Notions of structure

A special class of examples of this is the notion of structure in model theory. In this case one defines a “language” LL that describes the constants, functions (say operations) and relations with which we want to equip sets, and then sets equipped with those operations and relations are called LL-structures for that language. (Equivalently one might say “sets with LL-structure”. Or one might generally say “XX-structure” for “set with XX-structure”.) In this case there is a faithful functor from LL-structures to their underlying sets, and so this is a special case of the general definition.

We instead say model of a theory when we restrict to those structures which satisfy the axioms of a theory (in other words, satisfy properties specified by the axioms). In this case there is a full and faithful functor from the category of models of a theory TT to the category of structures of the underlying language L(T)L(T), while the composition of forgetful functors

Mod TStruct L(T)SetMod_T \to Struct_{L(T)} \to Set

is again faithful.


Thus, the English word “structure” is used in several slightly differing mathematical senses.

  1. Within category theory itself, “structure” can function as a kind of mass noun, as in a phrase like “forgetting structure”. Here it refers to data comprising operations, relations, constants, and also properties borne by models of a theory or relative theory, considered abstractly (for example, the functor GrpSetGrp \to Set which forgets group structure, or the functor RingAbRing \to Ab which forgets multiplicative structure). On the other hand, it can also operate in the singular, where one says for example “a topological group is a topological space equipped with a group structure, such that…”

  2. In model theory, however, the term structure is not a mass noun; it refers to a particular set (or “structures” for a family of sets) together with functions, relations, and elements that interpret the symbols of operations, predicates, and constants of a language. When one adds axioms to a language to make a theory, then a structure of the language where those axioms get interpreted as properties satisfied by the structure is called a model of the theory. Thus, in summary, the category theorist might refer to “the structure of a group” as consisting of a multiplication, a unit, etc., satisfying group axioms, while the model theorist would say that each particular group (like \mathbb{Z}) is a model of a theory of groups. For a model theorist, being a model does entail being a structure for the language of groups, but she would also say that a structure for the language of groups need not satisfy any of the axioms of a group (like associativity or unitality).


There are gazillions of examples of objects equipped with extra structure. The most familiar is maybe

Generally the forgetful functor from a category of algebras over an algebraic theory down to the base category exhibits the equipment with the corresponding algebraic structure.

Structures in dependent type theory

In dependent type theory the notion of “mathematical structure” and/or data structure on a base B:TypeB \,\colon\, Type is given by iterated dependent pairings (hence forming “type telescopes” also called “records” in Coq) with BB-dependent types encoding operations on/with this type together with their behavioural specification.

The following shows some examples, using the notation for dependent pairs from here.

Via the extensionality principles for dependent pairs (here) and for dependent functions (here) such type theoretic structure automatically obey the structure identity principle:

In that any equivalence/identification between pairs of data of the following types are isomorphisms in the sense of bijective homomorphisms.

Lensed data structure

To say that a given data (base) type B:SetB \,\colon\, Set is

  1. equipped with

    1. a function read D:BDread_D \,\colon\, B \to D reading out DD-data;

    2. a function write D:D×BBwrite_D \,\colon\, D \times B \to B (over-)writing DD-data;

  2. such that this does behave as expected, namely as a well-behaved DD-lens-structure on BB

means to declare it to be of the following iterated dependent pair-telescope type:

Group data structure

The dependent pair-telescope type declaration of group structure:

Further restriction to abelian groups:

Via the structure identity principle (above), the identitifications/equivalences between such group data types are indeed bijective group homomorphisms, hence group-isomorphisms:

The structure of subgroups of a given group structure:

and their underlying abstract group structure:

Group action structure

The dependent pair-telescope type declaration of group actions on sets (G-sets):

Specialization to torsors:

Ring data structure

The dependent pair-telescope type declaration of unital ring structure:

For examples see at numbersIn dependent type theory.

Module data structure

Given a unital ring type R:RingR \colon Ring (as above), the type of RR-module objects is the following dependent pair-telescope:

Higher structures in homotopy type theory

The above examples of structures formulated in dependent type theory all had data sets as their base, which is the classical situation. But in dependent type theory with untruncated identification types, hence in homotopy type theory, we may simply drop this constraint and consider structures whose base is any higher homotopy type: This yields the notion of higher structures.


Given a set-based group structure (as above), delooping structure is


Higher delooping

More generally, one may consider delooping of n n -groups, but this is a lot of (higher) structure if spelled out in detail. Yet more generally and again more readily axiomatized there is the notion of deloopings of any pointed types (cf. Wärn (2023, §2), BCFR23), which we may write as follows:

Similarly there is iterated delooping structure:



On the history of the notion of “mathematical structure” with some focus on what Bourbaki did and did not contribute to the subject:

  • Leo Corry, Mathematical Structures from Hilbert to Bourbaki: The Evolution of an Image of Mathematics, in: Changing Images of Mathematics in History. From the French Revolution to the new Millenium Harwood Academic Publishers (2001) 167-186 [ISBN:9780415868273, pdf]

  • Leo Corry, Modern Algebra and the Rise of Mathematical Structures, Springer (2004) [doi:10.1007/978-3-0348-7917-0]

See also

Early proposal to grasp the notion of mathematical structures via category theory (specifically via forgetful functors between groupoids):

For modern accounts on mathematical structures via categorical algebra see also at algebraic theory, monad, sketch.

In dependent type theory

Discussion of mathematical structures via dependent type theory:

the general idea of representing mathematical structures as type telescopes:

and with emphasis of the notion of isomorphism between such structures:

in Coq:

in Lean:

Discussion of classes of mathematical structures in univalent homotopy type theory (univalent foundations of mathematics) which satisfy a structure identity principle:

Discussion in the context of the philosophy of structuralism:

Expressions towards the notion that, thereby the notions of mathematical structures are data structures may be understood to coincide (just along the lines of types being data types):

“An example of a use case for non-binary sum types is the definition of mathematical “data structures” like a ring or a group. These data structures are usually defined as…”

Last revised on February 20, 2023 at 04:39:29. See the history of this page for a list of all contributions to it.