↑ Top

Properties of Terms and the Term Algebra

This is the Base.Terms.Properties module of the Agda Universal Algebra Library.


{-# OPTIONS --without-K --exact-split --safe #-}

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

module Base.Terms.Properties {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library --------------------------------------
open import Agda.Primitive          using () renaming ( Set to Type )
open import Data.Product            using ( _,_ ; Ξ£-syntax )
open import Function                using ( _∘_ )
open import Data.Empty.Polymorphic  using ( βŠ₯ )
open import Level                   using ( Level )
open import Relation.Binary         using ( IsEquivalence ; Setoid ; Reflexive )
                                    using ( Symmetric ; Transitive )
open import Relation.Binary.PropositionalEquality as ≑
                                    using ( _≑_ ; module ≑-Reasoning )
open import Axiom.Extensionality.Propositional
                                    using () renaming (Extensionality to funext)


-- Imports from the Agda Universal Algebra Library ----------------------------------------
open import Overture                using ( _⁻¹ ; 𝑖𝑑 ; ∣_∣ ; βˆ₯_βˆ₯ )
open import Base.Functions          using ( Inv ; InvIsInverseΚ³ ; Image_βˆ‹_)
                                    using ( eq ; IsSurjective )
open  import Base.Equality          using ( swelldef )

open  import Base.Algebras       {𝑆 = 𝑆} using ( Algebra ; _Μ‚_  ; ov )
open  import Base.Homomorphisms  {𝑆 = 𝑆} using ( hom )
open  import Base.Terms.Basic    {𝑆 = 𝑆} using ( Term ; 𝑻 )

open Term
private variable Ξ± Ξ² Ο‡ : Level

The universal property

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.


private variable X : Type Ο‡

free-lift : (𝑨 : Algebra Ξ±)(h : X β†’ ∣ 𝑨 ∣) β†’ ∣ 𝑻 X ∣ β†’ ∣ 𝑨 ∣
free-lift _ h (β„Š x) = h x
free-lift 𝑨 h (node f 𝑑) = (f Μ‚ 𝑨) (Ξ» i β†’ free-lift 𝑨 h (𝑑 i))

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 𝑑, the free lift is defined as follows: Assuming (the induction hypothesis) that we know the image of each subterm 𝑑 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 : (𝑨 : Algebra Ξ±) β†’ (X β†’ ∣ 𝑨 ∣) β†’ hom (𝑻 X) 𝑨
lift-hom 𝑨 h = free-lift 𝑨 h , Ξ» f a β†’ ≑.cong (f Μ‚ 𝑨) ≑.refl

Finally, we prove that the homomorphism is unique. This requires funext π“₯ Ξ± (i.e., function extensionality at universe levels π“₯ and Ξ±) which we postulate by making it part of the premise in the following function type definition.


open ≑-Reasoning

free-unique :  swelldef π“₯ Ξ± β†’ (𝑨 : Algebra Ξ±)(g h : hom (𝑻 X) 𝑨)
 β†’             (βˆ€ x β†’ ∣ g ∣ (β„Š x) ≑ ∣ h ∣ (β„Š x))
 β†’             βˆ€(t : Term X) β†’  ∣ g ∣ t ≑ ∣ h ∣ t

free-unique _ _ _ _ p (β„Š x) = p x

free-unique wd 𝑨 g h p (node 𝑓 𝑑) =
 ∣ g ∣ (node 𝑓 𝑑)    β‰‘βŸ¨ βˆ₯ g βˆ₯ 𝑓 𝑑 ⟩
 (𝑓 Μ‚ 𝑨)(∣ g ∣ ∘ 𝑑)  β‰‘βŸ¨ Goal ⟩
 (𝑓 Μ‚ 𝑨)(∣ h ∣ ∘ 𝑑)  β‰‘βŸ¨ (βˆ₯ h βˆ₯ 𝑓 𝑑)⁻¹ ⟩
 ∣ h ∣ (node 𝑓 𝑑)    ∎
  where
  Goal : (𝑓 Μ‚ 𝑨) (Ξ» x β†’ ∣ g ∣ (𝑑 x)) ≑ (𝑓 Μ‚ 𝑨) (Ξ» x β†’ ∣ h ∣ (𝑑 x))
  Goal = wd (𝑓 Μ‚ 𝑨)(∣ g ∣ ∘ 𝑑)(∣ h ∣ ∘ 𝑑)(Ξ» i β†’ free-unique wd 𝑨 g h p (𝑑 i))

Let’s account for what we have proved thus far about the term algebra. If we postulate a type X : Type Ο‡ (representing an arbitrary collection of variable symbols) such that for each 𝑆-algebra 𝑨 there is a map from X to the domain of 𝑨, then it follows that for every 𝑆-algebra 𝑨 there is a homomorphism from 𝑻 X to ∣ 𝑨 ∣ that β€œagrees with the original map on X,” by which we mean that for all x : X the lift evaluated at β„Š x is equal to the original function evaluated at x.

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 :  (𝑨 : Algebra Ξ±){hβ‚€ : X β†’ ∣ 𝑨 ∣}
 β†’                    IsSurjective hβ‚€ β†’ IsSurjective ∣ lift-hom 𝑨 hβ‚€ ∣

lift-of-epi-is-epi 𝑨 {hβ‚€} hE y = Goal
 where
 h₀⁻¹y = Inv hβ‚€ (hE y)

 Ξ· : y ≑ ∣ lift-hom 𝑨 hβ‚€ ∣ (β„Š h₀⁻¹y)
 η = (InvIsInverseʳ (hE y))⁻¹

 Goal : Image ∣ lift-hom 𝑨 hβ‚€ ∣ βˆ‹ y
 Goal = eq (β„Š h₀⁻¹y) Ξ·

The lift-hom and lift-of-epi-is-epi types will be called to action when such epimorphisms are needed later (e.g., in the Base.Varieties module).

← Base.Terms.Basic Base.Terms.Operations β†’