↑ Top

Properties of Terms and the Term Algebra

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

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

open import Algebras.Basic using ( π“ž ; π“₯ ; Signature )

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

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

-- Imports from the Agda Universal Algebra Library ----------------------------------------
open import Overture.Preliminaries      using ( _⁻¹ ; 𝑖𝑑 ; ∣_∣ ; βˆ₯_βˆ₯)
open import Overture.Inverses           using ( Inv ; InvIsInverseΚ³ ; Image_βˆ‹_; eq )
open import Overture.Surjective         using ( IsSurjective )
open import Equality.Welldefined        using ( swelldef )
open import Algebras.Basic              using ( Algebra ; _Μ‚_ )
open import Algebras.Products   {𝑆 = 𝑆} using ( ov )
open import Homomorphisms.Basic {𝑆 = 𝑆} using ( hom )
open import Terms.Basic         {𝑆 = 𝑆}

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 ∣ ∘ 𝑑)  β‰‘βŸ¨ wd (𝑓 Μ‚ 𝑨)(∣ g ∣ ∘ 𝑑)(∣ h ∣ ∘ 𝑑)(Ξ» i β†’ free-unique wd 𝑨 g h p (𝑑 i)) ⟩
 (𝑓 Μ‚ 𝑨)(∣ h ∣ ∘ 𝑑)  β‰‘βŸ¨ (βˆ₯ h βˆ₯ 𝑓 𝑑)⁻¹ ⟩
 ∣ h ∣ (node 𝑓 𝑑)    ∎

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

← Terms.Basic Terms.Operations β†’