↑ Top

Basic properties of terms on setoids

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

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

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

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

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive   using ( Level ) renaming ( Set to Type )
open import Data.Product     using ( _,_ )
open import Function.Bundles using () renaming ( Func to _⟢_ )
open import Function.Base    using ( _∘_ )
open import Relation.Binary  using ( Setoid )
open import Relation.Binary.PropositionalEquality as ≑ using (_≑_)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library ------------------------------------------------
open import Base.Overture.Preliminaries          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Base.Terms.Basic            {𝑆 = 𝑆}  using ( Term )

open import Setoid.Overture.Inverses             using ( Img_βˆ‹_ ; eq )
open import Setoid.Overture.Surjective           using ( isSurj ; IsSurjective ; isSurj→IsSurjective )
open import Setoid.Algebras.Basic       {𝑆 = 𝑆}  using ( Algebra ; π•Œ[_] ; _Μ‚_ )
open import Setoid.Homomorphisms.Basic  {𝑆 = 𝑆}  using ( hom ; compatible-map ; IsHom )
open import Setoid.Terms.Basic          {𝑆 = 𝑆}  using ( 𝑻 ; _≐_  ; ≐-isRefl )

open Term
open _⟢_ using ( cong ) renaming ( f to _⟨$⟩_ )

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 ; trans ) renaming ( Carrier to ∣A∣ )
 open Algebra (𝑻 X) using () renaming ( Domain to TX )
 open Setoid TX using () renaming ( Carrier 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
 cong free-lift-func = flcong
  where
  flcong : βˆ€ {s t} β†’ s ≐ t β†’  free-lift s β‰ˆ free-lift t
  flcong (_≐_.rfl x) = reflexive (≑.cong h x)
  flcong (_≐_.gnl x) = cong Interp (≑.refl , (Ξ» i β†’ flcong (x 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 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 Setoid.Terms.Properties, we needed function extensionality. Here, by using setoid equality, we can omit the swelldef hypothesis used to prove free-unique in the [Terms.Properties][] module.

module _ {𝑨 : Algebra Ξ± ρ}{gh hh : hom (𝑻 X) 𝑨} where

 open Algebra 𝑨 using ( Interp ) renaming ( Domain to A )
 open Setoid A using ( _β‰ˆ_ ; trans ; sym )
 open Algebra (𝑻 X) using () renaming ( Domain to TX )
 open _≐_
 open IsHom

 private
  g = _⟨$⟩_ ∣ gh ∣
  h = _⟨$⟩_ ∣ 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) = trans (trans geq lem3) (sym heq)
  where
  lem2 : βˆ€ i β†’ (g (t i)) β‰ˆ (h (t i))
  lem2 i = free-unique p (t i)

  lem3 : (f Μ‚ 𝑨)(Ξ» i β†’ (g (t i))) β‰ˆ (f Μ‚ 𝑨)(Ξ» i β†’ (h (t i)))
  lem3 = cong Interp (_≑_.refl , lem2)

  geq : (g (node f t)) β‰ˆ (f Μ‚ 𝑨)(Ξ» i β†’ (g (t i)))
  geq = compatible βˆ₯ gh βˆ₯

  heq : h (node f t) β‰ˆ (f Μ‚ 𝑨)(Ξ» i β†’ h (t i))
  heq = compatible βˆ₯ hh βˆ₯

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