---
layout: default
title : "Overture.Terms.Basic module (The Agda Universal Algebra Library)"
date : "2026-06-18"
author: "agda-algebras development team"
---

## Terms over a signature {#terms}

A `Term X` is a finite tree whose leaves are drawn from a type `X` of variable
symbols and whose internal nodes are labelled by operation symbols of the signature
`š‘†`.  Equivalently, `Term` is the W-type for the polynomial functor associated to
`š‘†`, freely adjoined a copy of `X` at the leaves.

This definition presupposes only the signature: no propositional equality on a
carrier, no setoid equivalence, no path type.  It is therefore foundational rather
than setoid-specific, which is why it lives in `Overture/` rather than under
`Setoid/`, `Classical/`, or `Cubical/`.  The Setoid term algebra `š‘» X` (which equips
`Term X` with an inductive equivalence-of-terms relation `_ā‰_`) is built on top of
this definition in `Setoid.Terms.Basic`; the planned Cubical analog will sit
similarly.[^1]

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture.Signatures using ( š“ž ; š“„ ; Signature )

module Overture.Terms.Basic {š‘† : Signature š“ž š“„} where
open import Agda.Primitive       using () renaming ( Set to Type )
open import Level                using ( Level ; suc ; _āŠ”_ )
open import Overture.Signatures  using ( OperationSymbolsOf ; ArityOf )
private variable Ļ‡ : Level
```
-->

### The level shorthand `ov`

Throughout the library we package the universe levels of operation symbols (`š“ž`),
arities (`š“„`), and a separate "carrier-or-variable" level (`Ļ‡`) into a single
shorthand `ov Ļ‡ = š“ž āŠ” š“„ āŠ” suc Ļ‡`.  The `suc` is unavoidable because `Term X` mixes
leaves of type `X : Type Ļ‡` with operation symbols of type `Type š“ž`, so the resulting
tree type sits one universe up.

This shorthand currently appears with the same definition in
`Legacy.Base.Algebras.Basic` and `Setoid.Algebras.Basic`; the three definitions are
definitionally equal.[^2]

```agda
ov : Level ā†’ Level
ov Ļ‡ = š“ž āŠ” š“„ āŠ” suc Ļ‡
```

### The type of terms

Fix a signature `š‘†` and let `X` denote an arbitrary collection of variable symbols,
assumed disjoint from the operation symbols of `š‘†`
(i.e. `X āˆ© OperationSymbolsOf š‘† = āˆ…`).

By a *word* in the language of `š‘†`, we mean a nonempty finite sequence of members of
`X āˆŖ OperationSymbolsOf š‘†`; we denote concatenation of such sequences by simple
juxtaposition.

Let `Sā‚€` denote the set of nullary operation symbols of `š‘†`.  We define the sets `š‘‡ā‚™`
of *words* over `X āˆŖ OperationSymbolsOf š‘†` by induction on `n`
(cf. [Bergman (2012)][] Def. 4.19):

`š‘‡ā‚€ := X āˆŖ Sā‚€`  and  `š‘‡ā‚™ā‚Šā‚ := š‘‡ā‚™ āˆŖ š’Æā‚™`

where `š’Æā‚™` is the collection of all `f t` such that `f : OperationSymbolsOf š‘†` and `t
: ArityOf š‘† f ā†’ š‘‡ā‚™` (recall `ArityOf š‘† f` is the arity of `f`).  The collection of
*terms* in the signature `š‘†` over `X` is then `Term X := ā‹ƒā‚™ š‘‡ā‚™`.  By an š‘†-*term* we
mean a term in the language of `š‘†`.

The definition of `Term X` is recursive, indicating that an inductive type suffices
to represent the notion in type theory.  Such a representation is given by the
inductive type below, which encodes each term as a tree with an operation symbol at
each `node` and a variable symbol (the `generator`) at each leaf.

```agda
data Term (X : Type Ļ‡) : Type (ov Ļ‡) where
  ā„Š     : X ā†’ Term X                            -- ā„Š is for "generator"
  node  : (f : OperationSymbolsOf š‘†)(t : ArityOf š‘† f ā†’ Term X) ā†’ Term X

open Term public
```

**Notation**.  The type `X` represents an arbitrary collection of variable symbols;
`ov Ļ‡` is the universe-level shorthand defined above.

The bare-types term algebra `š‘» : (X : Type Ļ‡) ā†’ Algebra (ov Ļ‡)`, which equips `Term
X` with `node` as its interpretation, is *not* relocated here: it depends on the
foundation-specific `Algebra` type, which differs between the bare-types tree
(`Legacy.Base.Algebras.Algebra`) and the canonical Setoid tree
(`Setoid.Algebras.Basic.Algebra`).  The legacy `š‘»` continues to live in
`Legacy.Base.Terms.Basic`; the Setoid term algebra continues to live in
`Setoid.Terms.Basic`.

--------------------------------------

[^1]: This module is a Category-A relocation under #303 (M2-6).  See [`src/Legacy/Base/DEPRECATED.md`](../Legacy/Base/DEPRECATED.md) for the full inventory.

[^2]: Hoisting `ov` to `Overture.Signatures` and removing the duplicates is a small candidate cleanup tracked separately from #303.