---
title: "Mapping constants"
module: FOL.Manipulation.ConstantMapping
lang: en
site: "Bedrock"
description: "Mapping constants"
stage: "First-order logic"
reading_order: 12
canonical: https://bedrock.institute/en/FOL.Manipulation.ConstantMapping.html
html: FOL.Manipulation.ConstantMapping.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/ConstantMapping.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax]
routes: [fol-operations]
translations: [https://bedrock.institute/zh/FOL.Manipulation.ConstantMapping.md, https://bedrock.institute/ja/FOL.Manipulation.ConstantMapping.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Mapping constants

A function between constant domains acts on first-order syntax by replacing every constant symbol and leaving every variable untouched. This chapter defines that action on terms and formulas, proves that it respects composition, and specializes the formula map to carry parameter-free formulas, whose constant domain is the empty type, into formulas over any constant domain.

A formula such as `var 0 ∈̇ con k` names two things in two different ways: `var 0` refers through the free variables, while `con k` refers through the constant domain, some type `K`. Now suppose we are given a function `f : K → K'`. What should the relabelled formula look like? The natural answer is that only the constant moves: `con k` becomes `con (f k)`, while the variable, the membership relation, and the overall shape of the formula stay exactly as they were. This chapter defines that relabelling on terms and then on formulas, working with the types `Term` and `Formula` from the syntax chapter and their full stock of constructors: the atomic relations `_∈̇_` and `_≐_`, the connectives, and the quantifiers including the bounded forms `∀̇∈` and `∃̇∈`.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.ConstantMapping where

open import Base.Prelude
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
```

One special choice of domain will deserve its own attention: the empty type `⊥*`. A formula whose constant domain is `⊥*` contains no constants at all, and the end of this chapter studies how such formulas map into formulas over any `K`. Until then, everything takes place for an arbitrary function between constant domains.

```agda
import Cubical.Data.Empty as Empty
```

## Syntax level

The syntax is functorial in its constant domain: a map `K → K'` pushes through a term or formula, relabelling constants while preserving de Bruijn variables and logical structure. This section defines that action; the composition law is proved in the next section.

On terms the action leaves no room for choice. `mapTm` takes the relabelling function `f : K → K'` and a term of free-variable arity `n`, and returns a term of the same arity `n`: the constant `con k` becomes `con (f k)` and the variable `var i` is returned unchanged. This is a relabelling of constant symbols only; it is not substitution and has no effect on variables.

```agda
mapTm : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Term K n → Term K' n
mapTm f (con k) = con (f k)
mapTm f (var i) = var i

mapFo : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
```

An atomic formula shows how the action extends to formulas. The image of `t ∈̇ u` under `mapFo` is `mapTm f t ∈̇ mapTm f u`: the same relation applied to the two mapped terms, over the same arity `n`. So the running example `var 0 ∈̇ con k` maps to `var 0 ∈̇ con (f k)`, in which only the constant has moved.

```agda
      → (K → K') → Formula K n → Formula K' n
mapFo f (t ∈̇ u)  = mapTm f t ∈̇ mapTm f u
mapFo f (t ≐ u)  = mapTm f t ≐ mapTm f u
mapFo f (φ ∧̇ ψ)  = mapFo f φ ∧̇ mapFo f ψ
mapFo f (φ ∨̇ ψ)  = mapFo f φ ∨̇ mapFo f ψ
```

A quantified formula shows that logical structure is untouched. Under `mapFo`, a quantifier prefix is kept and its body, of arity `suc n`, is mapped recursively and returned with the same arity; each connective is rebuilt on the mapped subformulas. The operation neither adds nor removes a binder, and no constructor ever changes shape; falsity `⊥̇`, which carries no constant, maps to itself.

```agda
mapFo f (φ ⇒̇ ψ)  = mapFo f φ ⇒̇ mapFo f ψ
mapFo f ⊥̇        = ⊥̇
mapFo f (∃̇ φ)    = ∃̇ mapFo f φ
mapFo f (∀̇ φ)    = ∀̇ mapFo f φ
mapFo f (∀̇∈ t φ) = ∀̇∈ (mapTm f t) (mapFo f φ)
```

The bounded quantifiers `∀̇∈` and `∃̇∈` are the case where both operations meet, since they combine a term with a formula: the bounding term `t` is relabelled by `mapTm` and the body by `mapFo`. With this, `mapFo` transforms syntax only; it never interprets a formula or touches an environment.

```agda
mapFo f (∃̇∈ t φ) = ∃̇∈ (mapTm f t) (mapFo f φ)
```

Two such maps in a row are one map: mapping by `f` and then by `g` agrees, as a path, with mapping once by `λ k → g (f k)`. This functoriality of the constant-domain action is what later chapters use to collapse an intermediate constant domain, and it belongs to the syntax level rather than to any one application.

The composition law is a commuting square. If a term is mapped first along `f : K → K'` and then along `g : K' → K''`, the result should agree with mapping it once along the composite `λ k → g (f k)`. `mapTm-comp` states exactly this, as a path in `Term K'' n`. On a constant, both sides compute to `con (g (f k))`, so the agreement already holds as definitional equality and `refl` proves the case; on a variable no constant occurs, so the two sides are again the same term.

```agda
mapTm-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (t : Term K n)
           → mapTm g (mapTm f t) ≡ mapTm (λ k → g (f k)) t
mapTm-comp f g (con k) = refl
mapTm-comp f g (var i) = refl
```

For formulas the same square is stated by `mapFo-comp`: the two routes around the square, `mapFo g (mapFo f φ)` and `mapFo (λ k → g (f k)) φ`, are paths of the same type `Formula K'' n`. Since the square is already proved for terms, the atomic cases need no new argument on terms: congruence `cong₂` lifts the two term paths into a path between the rebuilt atoms.

```agda
mapFo-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (φ : Formula K n)
           → mapFo g (mapFo f φ) ≡ mapFo (λ k → g (f k)) φ
mapFo-comp f g (t ∈̇ u)  = cong₂ _∈̇_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (t ≐ u)  = cong₂ _≐_ (mapTm-comp f g t) (mapTm-comp f g u)
```

Structural recursion propagates the square through the connectives: each subformula carries its own instance, and congruence rebuilds the connective on the two subformula paths. Falsity `⊥̇` contains neither constants nor subformulas, so both routes compute to the same formula and the case is `refl`.

```agda
mapFo-comp f g (φ ∧̇ ψ)  = cong₂ _∧̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ∨̇ ψ)  = cong₂ _∨̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g ⊥̇        = refl
mapFo-comp f g (∃̇ φ)    = cong ∃̇_ (mapFo-comp f g φ)
```

The quantifier cases close the induction: a prefix quantifier applies to one subformula, while the bounded forms `∀̇∈` and `∃̇∈` pair a term with a body and use both the term path and the body path. Since every constructor of `Formula` is covered, the composition square commutes for every formula. This functoriality is a purely syntactic fact, available wherever later chapters need to collapse an intermediate constant domain.

```agda
mapFo-comp f g (∀̇ φ)    = cong ∀̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇∈ t φ) = cong₂ ∀̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
mapFo-comp f g (∃̇∈ t φ) = cong₂ ∃̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
```

The most frequently used instance of the map enters a constant domain from **no** constants. The syntax chapter introduced the **parameter-free formulas**, whose constant domain is the empty type; like sentences they have no separate name, and the type `Formula (⊥* {ℓ}) n` expresses the full definition: a formula of this type contains no constant nodes at all, but may still use any of its `n` available free-variable slots. Relabelling into a type `K` requires a function `⊥* → K`, and the empty type is exactly the type for which such a function exists uniquely, with no case to define: there is no constant to send anywhere. This is what the eliminator `Empty.rec*` provides, and relabelling along it maps parameter-free formulas into formulas over any domain.

`embed` is exactly `mapFo Empty.rec*`: the unique function `⊥* → K` from the empty constant alphabet is used as the relabelling, so every constant position, of which there are none, is sent somewhere. What changes is the constant domain alone: the free-variable context of length `n` and the binders are untouched, so `embed` neither closes the formula nor supplies an environment for its variables.

```agda
embed : ∀ {ℓ ℓ'} {K : Type ℓ'} {n} → Formula (⊥* {ℓ}) n → Formula K n
embed = mapFo Empty.rec*
```

## Recap

`mapTm` and `mapFo` express the syntax-level action of a map of constant domains: constants are relabelled, variables, binders and arities are untouched. `mapFo-comp` proves this action is functorial under composition, and `embed` is the parameter-free instance, the basis for later constant relabelling and parameter abstraction.