Univalent mathematics and homotopy type theory provide a structural approach to formalizing mathematical concepts. Inspired by the role of displayed categories in the univalent treatment of category theory, we develop an analogous notion of displayed algebras for universal algebra. This modular and layered approach allows us to construct and reason about algebraic structures over a fixed base. Classical constructions such as cartesian products, pullbacks, semidirect products, and subalgebras naturally arise as total algebras of suitable displayed algebras. The main results are fully formalized in the UniMath library.
and infrastructure for developing universal algebra in a modular and structured way. Moreover, the library also ofers many implementations of algebraic structures (groups, ordered sets, . . . ) which may be presented as instances of our constructions.
In this context, our goal is to develop a formalization of Universal Algebra that is naturally aligned with the principles and foundational philosophy of univalent mathematics in UniMath.
Both universal algebra and category theory provide unifying frameworks for studying algebraic
structures in abstract terms [
In universal algebra, a structure – be it a group, a ring, or a lattice – is described as a theory, i.e. in
terms of abstract operations over a carrier and a set of equations these operations are required to satisfy.
This way, once a theory is specified, specific instances of algebraic structures are defined as models of
that theory, and an algebra homomorphism is a structure-preserving map between models [
In category theory, Lawvere theories provide a presentation-invariant version of algebraic theories,
where algebraic operations are given by morphisms in the Lawvere theory. Specific instances of
algebraic structures are defined as product-preserving functors from a Lawvere theory to categories
with finite products. This reveals universal algebra as the theory of all structures that can be defined in
categories with finite products [
The work started with [
Concretely, given a base algebra, we display the additional algebraic structure – elements and operations – in a structured layer above such base. This approach not only streamlines proofs of properties and constructions but also facilitates the reuse of generic lemmas across diferent algebraic contexts. This way we can reap the organizational benefits of displayed formalisms, both for the mathematical developments of universal algebra and their computer implementations.
Our code is freely available from our GitHub repository1 and it is already integrated in the oficial UniMath library. When discussing concepts which are available in our source code, we will provide specific links below, denoted by the icon 2.
This work extends our previous development [
We report here some of the key constructions of our development. We refer to our earlier work for further details. We start with the basic definition of signature and algebra. We require that the type of sorts has a decidable equality and that the type of operations is an hSet (a set in the homotopical sense).
Definition signature 2 : UU := ∑︀ (S: decSet) (O: hSet), O → list S × S. Definition algebra 2 ( : signature): UU
:= ∑︀ A: sUU (sorts ), ∏︀ nm: names , A⋆ (arity nm) → A (sort nm).
The construction of the algebra of terms is based on the idea of a stack machine that we roughly sketch below: 1. A sequence of function symbols is thought of as a series of commands to be executed by a stack machine whose stack is made of sorts, and which we define by means of a maybe monad.
Definition oplist 2 ( : signature):= list (names ).
Definition stack 2 ( : signature): UU := maybe (list (sorts )). 2. When an operation symbol is executed, its arity is popped out from the stack and replaced by its range. When a stack underflow occurs, or when the sorts present in the stack are not the ones expected by the operator, the stack goes into an error condition which is propagated by successive operations. We implement this process by means of two functions:
Definition opexec 2 (nm: names ): stack → stack .
Definition oplistexec 2 (l: oplist ): stack .
The former is the stack transformation corresponding to the execution of the operation symbol nm. The latter returns the stack corresponding to the execution of the entire oplist argument starting from the empty stack. The list is executed from the last to the first operation symbol. Several additional lemmas are required in order to make us able to handle stacks – by concatenating, splitting, etc. – without incurring failures breaking down the whole process.2 3. Finally, we define a term to be just a list of operation symbols that, after being executed by oplistexec, returns a list of length one with appropriate sort:3
Definition isaterm 2 (s: sorts ) (l: oplist ): UU
:= oplistexec l = just [s].
Definition term 2 ( : signature) (s: sorts ): UU
:= ∑︀ t: oplist , isaterm s t.
The natural starting point of our work is the formal definition of displayed algebras. Definition. Given an algebra ℬ over a multi-sorted signature , a displayed algebra 2 over ℬ consists of: · a family of “fiber” types indexed over terms of ℬ; · a family of “overop“ functions indexed over any operation name of and any vector of terms of ℬ each having the appropriate sort specified by the arity of . Each function has the product of the ifber of the components of as domain and the fiber of ℬ() as codomain.
This is depicted in the following: 2In particular, since we need to decide when a stack is correctly executed and when an underflow occurs, we see the reasons for choosing sorts to constitute a decidable set. 3From a purely HoTT-perspective, we can easily see also that the type of stacks over is an hSet, so that the property of being a term is not proof-relevant (isapropisaterm 2).
ifb( 1) ifb( 2)
ifb( ℬ()) 1 2 overop ℬ ℬ
Unfortunately, formalized mathematics sometimes makes obscure concepts which are otherwise quite natural. The formal definition of a displayed algebra in UniMath is the following: Definition disp_alg 2 { : signature} (B: algebra ) := ∑︀ fib : (∏︀ (s: sorts ) (b: support B s), UU), ∏︀ (nm: names ) (base_xs: hvec (vec_map B (arity nm))), hvec (h1map_vec (v := arity nm) fib base_xs) → fib (sort nm) (ops B nm (base_xs)).
In a straightforward and natural way, every displayed category gives rise to a total category. Analogously, from a displayed algebra we can build the associated total algebra 2. The carriers are dependent pairs with the carriers of ℬ in the first component and the fiber types in the second one. Operations are built from the ones of ℬ and the overop functions.
Definition total_alg 2 {A: algebra } (D: disp_alg A) : algebra .
This construction is one of the primary motivations for working with displayed structures since it provides a clear, modular framework for assembling algebras from simpler components.
In the categorical setting, a displayed category encodes the same information as a functor into the base category. In our algebraic setting, we show the analogous result 2: Theorem. Given an algebra ℬ over a multi-sorted signature with hSet carriers , the type of algebra morphisms targetting ℬ is equivalent to the type of displayed algebras over ℬ.
Proof sketch. From any homomorphism ℎ targeting ℬ, we construct the displayed algebra of its fibers 2. Fiber types are given by the fiber under ℎ of the specific index term, and overop functions are derived from the operations in the source algebra: their well-typedness depends on the fact that ℎ is a homomorphism.
On the other hand taking the projections on the first component of the total algebra carriers leads to the definition of the forgetful homomorphism 2.
We finally show that taking the displayed algebra of the fiber and taking the forgetful homomorphism of a total algebra are operations inverse to each other. This also requires verifying higher coherence conditions between the type components of the whole construction.
This final step is both conceptually and technically the most delicate part of the development: it has no direct analogue in classical mathematics, as it relies crucially on the dependent and homotopical nature of types in univalent foundations. The argument is relatively long and involves managing multiple layers of dependent data and coherence, which would be invisible or collapsed in a set-theoretic setting.
We emphasize how various familiar algebraic constructions – in particular, those admitting a staged or layered description – can be systematically recovered by taking the total algebra of a displayed algebra. Here are some examples: Cartesian Products: A displayed algebra can encode how algebraic operations behave componentwise on a product of carriers. Collecting these componentwise structures into a single object yields the familiar cartesian product algebra 2 as its total algebra.
Pullbacks: By generalizing the previous example, one can display algebraic structure along pullback squares to obtain a pullback of algebras. The resulting total algebra thus inherits its operations from the displayed structure, reflecting the universal property of the pullback on the level of algebras.
Semidirect Products: The semidirect product of groups can also be viewed as the total algebra of a suitable displayed algebra. Here, one “displays” how a normal subgroup and a quotient group interact, and then reassembles this information into the total structure defining the semidirect product.4 Subalgebras: Consider a displayed algebra that restricts the underlying carriers of a larger algebra to subsets closed under its operations. When one collects this restricted (or “sub”) structure into a single object, the total algebra precisely captures 2 the notion of a subalgebra 2.
This paper builds upon our original UniMath library for universal algebra [
Our novel implementation of displayed algebras is inspired by the work in displayed categories
started with [
This work was partially supported by: the project SERICS ‘Security and Rights in CyberSpace’ – PE0000014, financed within PNRR, M4C2 I. 1. 3, funded by the European Union - NextGenerationEU; the MIUR project PRIN 2017JZ2SW5 ‘Real and Complex Manifolds: Topology, Geometry and holomorphic dynamics’; the PNRR project FAIR – Future AI Research (PE00000013), Spoke 9 - Green-aware AI, under the NRRP MUR program funded by the NextGenerationEU; Istituto Nazionale di Alta Matematica – INdAM groups GNAMPA, GNCS and GNSAGA.
During the preparation of this work, the authors used X-GPT-4 to: Drafting content, Paraphrase and
reword, Improve writing style. After using these tools, the authors reviewed and edited the content as
needed and take full responsibility for the publication’s content.
4While semidirect products of groups have well-known generalizations to other contexts in universal algebra [
doi:10.5281/zenodo.5765793, documentation available at https://ualib.org. [27] A. Lynge, Universal algebra in HoTT, 2017. URL: https://github.com/andreaslyn/Work/blob/master/
Math-Bachelor.pdf, bachelor’s thesis, Department of Mathematics, Aarhus University. [28] A. Lynge, B. Spitters, Universal algebra in HoTT, in: TYPES 2019, 25th International Conference on Types for Proofs and Programs, 2019, pp. 1–2. URL: http://www.ii.uib.no/~bezem/abstracts/ TYPES_2019_paper_7.