Skip to content

Setoid.Terms.Properties

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 extends h to all of 𝑻 X by structural recursion,
  • free-lift-func shows the extension respects term equality,
  • lift-hom shows the extension is a homomorphism,
  • free-unique 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: a map on variables extends to a homomorphism, and to only one. The existence half is used in Setoid.Varieties.HSP where lift-hom maps the term algebra into each algebra of a class.

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

{-# 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.

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.

  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.

  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.

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:

                  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.)

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ᡇ)