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.
π
to β£ π¨ β£
lifts to a homomorphism from π» X
to π¨
.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 β₯