---
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][].


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

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Terms.Properties {𝑆 : Signature π“ž π“₯} 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β‚‚ )
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 prove this in [Agda][], 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 _ {𝑨 : 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
[Basic.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 _ {𝑨 : 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 _ {𝑨 : 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ᡇ)
```