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.

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

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.

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

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:

                  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 _ {𝑨 : 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ᡇ)