↑ 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 Overture using (π“ž ; π“₯ ; Signature)

module Setoid.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 ( _,_ )
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 as ≑ using (_≑_)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Functions  using ( Img_βˆ‹_ ; eq ; isSurj ; IsSurjective )
                              using ( isSurj→IsSurjective )

open import Base.Terms            {𝑆 = 𝑆} using ( Term )
open import Setoid.Algebras       {𝑆 = 𝑆} using ( Algebra ; π•Œ[_] ; _Μ‚_ )
open import Setoid.Homomorphisms  {𝑆 = 𝑆} 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 [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 ( _β‰ˆ_ ; 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 β†’