---
layout: default
title : "Setoid.Terms.Properties module (The Agda Universal Algebra Library)"
date : "2021-09-18"
author: "agda-algebras development team"
---

#### Basic properties of terms on setoids

This is the [Setoid.Terms.Properties][] module of the [Agda Universal Algebra Library][].

This module proves that the term algebra is **free**.

Given an algebra `𝑨` and an arbitrary map `h : X β†’ π•Œ[ 𝑨 ]` sending variables to
elements,

+  `free-lift`{.AgdaFunction} extends `h` to all of `𝑻 X` by structural recursion,
+  `free-lift-func`{.AgdaFunction} shows the extension respects term equality,
+  `lift-hom`{.AgdaFunction} shows the extension is a homomorphism,
+  `free-unique`{.AgdaFunction} supplies the other half of the universal property:
   two homomorphisms out of `𝑻 X` that agree on the variables agree everywhere.

Together the last two are the universal property of `𝑻 X`{.AgdaFunction}: a map on
variables extends to a homomorphism, and to only one.  The existence half is used
in [Setoid.Varieties.HSP][] where `lift-hom`{.AgdaFunction} maps the term algebra
into each algebra of a class.

`free-unique`{.AgdaFunction} is a terminal result here, with no consumer in
the live trees at present.  `lift-of-epi-is-epi`{.AgdaFunction} records that
surjectivity of the variable assignment survives the lift, which is how
epimorphisms out of the term algebra are obtained.

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

module Setoid.Terms.Properties where

open import Agda.Primitive   using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Product                           using ( _,_ )
open import Function.Bundles                       using () renaming ( Func to _⟢_ )
open import Function.Base                          using ( _∘_ )
open import Level                                  using ( Level )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( setoid; cong; refl)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture              using  ( proj₁ ; projβ‚‚ ; π“ž ; π“₯ ; Signature ; 𝑆 )
open import Overture.Terms        using  ( Term )
open import Setoid.Algebras       using  ( Algebra ; π•Œ[_] ; 𝔻[_] ; _^_ )
open import Setoid.Functions      using  ( Img_βˆ‹_ ; eq ; isSurj ; IsSurjective
                                         ; isSurj→IsSurjective )
open import Setoid.Homomorphisms  using  ( hom ; compatible-map ; IsHom ; βŠ™-hom )
open import Setoid.Terms.Basic    using  ( 𝑻 ; _≐_  ; ≐-isRefl )

open Term
open _⟢_ using () renaming ( to to _⟨$⟩_ ; cong to β‰ˆcong )

private variable
  Ξ± ρᡃ Ξ² ρᡇ ρ Ο‡ : Level
  X : Type Ο‡
```
-->

The term algebra `𝑻 X` is *absolutely free* (or *universal*, or *initial*) for
algebras in the signature `𝑆`. That is, for every 𝑆-algebra `𝑨`, the following hold.

1. Every function from `𝑋` to `π•Œ[ 𝑨 ]` lifts to a homomorphism from `𝑻 X` to `𝑨`.
2. The homomorphism that exists by item 1 is unique.

We now formalize this, starting with the fact that every map from `X` to `π•Œ[ 𝑨 ]`
lifts to a map from `π•Œ[ 𝑻 X ]` to `π•Œ[ 𝑨 ]` in a natural way, by induction on the
structure of the given term.

```agda
module _ {𝑆 : Signature π“ž π“₯}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ}(h : X β†’ π•Œ[ 𝑨 ]) where
  open Algebra 𝑨              using ( Interp ) renaming ( Domain to A )
  open Setoid A               using ( _β‰ˆ_ ; reflexive )
  open Algebra (𝑻 {𝑆 = 𝑆} X)  using () renaming ( Domain to TX )

  free-lift : π•Œ[ 𝑻 {𝑆 = 𝑆} X ] β†’ π•Œ[ 𝑨 ]
  free-lift (β„Š x) = h x
  free-lift (node f t) = (f ^ 𝑨) (Ξ» i β†’ free-lift (t i))

  free-lift-of-surj-isSurj :
    isSurj{𝑨 = setoid X}{𝑩 = A} h β†’ isSurj{𝑨 = TX}{𝑩 = A} free-lift
  free-lift-of-surj-isSurj hE {y} = mp p
    where
    p : Img h βˆ‹ y
    p = hE
    mp : Img h βˆ‹ y β†’ Img free-lift βˆ‹ y
    mp (eq a x) = eq (β„Š a) x

  free-lift-func : TX ⟢ A
  free-lift-func ⟨$⟩ x = free-lift x
  free-lift-func .β‰ˆcong = flcong
    where
    open _≐_
    flcong : βˆ€ {s t} β†’ s ≐ t β†’  free-lift s β‰ˆ free-lift t
    flcong (rfl x≑y) = reflexive (cong h x≑y)
    flcong (gnl s≐t) = β‰ˆcong Interp (refl , flcong ∘ s≐t)
```

Naturally, at the base step of the induction, when the term has the form `generator`
x, the free lift of `h` agrees with `h`.  For the inductive step, when the given term
has the form `node f t`, the free lift is defined as follows: Assuming (the induction
hypothesis) that we know the image of each subterm `t i` under the free lift of `h`,
define the free lift at the full term by applying `f ^ 𝑨` to the images of the subterms.

The free lift so defined is a homomorphism by construction. Indeed, here is the trivial proof.

```agda
  lift-hom : hom (𝑻 X) 𝑨
  lift-hom = free-lift-func , hhom
    where
    hfunc : TX ⟢ A
    hfunc = free-lift-func

    hcomp : compatible-map (𝑻 X) 𝑨 free-lift-func
    hcomp {f}{a} = β‰ˆcong Interp (refl , (Ξ» i β†’ (β‰ˆcong free-lift-func){a i} ≐-isRefl))

    hhom : IsHom (𝑻 X) 𝑨 hfunc
    hhom = record { compatible = Ξ»{f}{a} β†’ hcomp{f}{a} }
```

If we further assume that each of the mappings from `X` to `π•Œ[ 𝑨 ]` is *surjective*,
then the homomorphisms constructed with `free-lift` and `lift-hom` are
*epimorphisms*, as we now prove.

```agda
  lift-of-epi-is-epi : isSurj{𝑨 = setoid X}{𝑩 = A} h β†’ IsSurjective free-lift-func
  lift-of-epi-is-epi hE = isSurj→IsSurjective free-lift-func (free-lift-of-surj-isSurj hE)
```

Finally, we prove that the homomorphism is unique.  Recall, when we proved this in the module
[Legacy.Base.Terms.Properties][], we needed function extensionality. Here, by using setoid equality,
we can omit the `swelldef` hypothesis we needed previously to prove `free-unique`.


```agda
module _ {𝑆 : Signature π“ž π“₯}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ}{gh hh : hom (𝑻 X) 𝑨} where
  open Algebra 𝑨              using ( Interp )  renaming ( Domain to A )
  open Setoid A               using ( _β‰ˆ_ )
  open Algebra (𝑻 {𝑆 = 𝑆} X)  using ()          renaming ( Domain to TX )
  open SetoidReasoning A
  open _≐_
  open IsHom

  private
    g h : TX ⟢ A
    g = proj₁ gh
    h = proj₁ hh
  free-unique : (βˆ€ x β†’ g ⟨$⟩ (β„Š x) β‰ˆ h ⟨$⟩ (β„Š x)) β†’ βˆ€ (t : Term {𝑆 = 𝑆} X) β†’  g ⟨$⟩ t β‰ˆ h ⟨$⟩ t
  free-unique p (β„Š x) = p x
  free-unique p (node f t) = begin
    g ⟨$⟩ (node f t)              β‰ˆβŸ¨ compatible (projβ‚‚ gh) ⟩
    (f ^ 𝑨)(Ξ» i β†’ (g ⟨$⟩ (t i)))  β‰ˆβŸ¨ β‰ˆcong Interp (refl , Ξ» i β†’ free-unique p (t i)) ⟩
    (f ^ 𝑨)(Ξ» i β†’ (h ⟨$⟩ (t i)))  β‰ˆΛ˜βŸ¨ compatible (projβ‚‚ hh) ⟩
    h ⟨$⟩ (node f t)              ∎
```


##### Naturality of the free lift

Existence (`lift-hom`) and uniqueness (`free-unique`) together say that `𝑻 X` is a
*free* (initial) object, and freeness always brings a third, slightly less quotable
property: the assignment "generator map ↦ induced homomorphism" is *natural* in the
target algebra.  Concretely, lifting `Ξ· : X β†’ π•Œ[ 𝑨 ]` into `𝑨` and then applying a
homomorphism `h : 𝑨 ⟢ 𝑩` is the same as lifting the composite map `h ∘ Ξ·` into `𝑩`
directly:

```text
                  lift-hom Ξ·
        𝑻 X ────────────────────→ 𝑨
            β•²                     β”‚
             β•²                    β”‚ h
   lift-hom   β•²                   β”‚
   (h ∘ Ξ·)     β†˜                  ↓
                                  𝑩
```

The proof is a one-liner, and *that* is the point: both routes around the triangle
are homomorphisms `𝑻 X ⟢ 𝑩` that agree on the generators (both send `β„Š x` to
`h (Ξ· x)`, definitionally), so `free-unique` forces them to agree on every term.  No
induction over terms appears here β€” it is already packaged inside `free-unique`.
This is the way category theory pays rent: theorems about *all* terms become
theorems about *generators only*.

(The same fact in environment form β€” `h (⟦ t ⟧ a) β‰ˆ ⟦ t ⟧ (h ∘ a)` β€” is
`comm-hom-term` in [Setoid.Terms.Operations][], proved there by direct induction;
`free-lift-interp`, also in that module, mediates between the two phrasings.  The
companion naturality in the *signature* argument, where the algebra is fixed and the
signature varies along a morphism, is `reduct-interp` in
[Setoid.Varieties.Invariance][].)

```agda
module _ {𝑆 : Signature π“ž π“₯}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}{𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ}(h : hom 𝑨 𝑩)(Ξ· : X β†’ π•Œ[ 𝑨 ]) where
  open Setoid 𝔻[ 𝑩 ] using () renaming ( _β‰ˆ_ to _β‰ˆα΅‡_ ; refl to reflᡇ )

  free-lift-natural : (t : Term {𝑆 = 𝑆} X)
   β†’                  proj₁ h ⟨$⟩ free-lift{𝑨 = 𝑨} Ξ· t β‰ˆα΅‡ free-lift{𝑨 = 𝑩} (Ξ» x β†’ proj₁ h ⟨$⟩ Ξ· x) t

  free-lift-natural =
   free-unique {𝑨 = 𝑩} {gh = βŠ™-hom (lift-hom Ξ·) h} {hh = lift-hom (Ξ» x β†’ proj₁ h ⟨$⟩ Ξ· x)}
    (Ξ» _ β†’ reflᡇ)
```