↑ Top


Free setoid algebras

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

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

module Varieties.Func.FreeAlgebras {𝑆 : 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 ; _,_ ) renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Function         using ( _∘_ ; id )
open import Function.Bundles using ( Func )
open import Level
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( Pred ; _∈_ ; _βŠ†_ )
open import Relation.Binary.PropositionalEquality as ≑ using (_≑_)

-- Imports from the Agda Universal Algebra Library ---------------------------------------------------
open import Overture.Preliminaries                  using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Overture.Func.Preliminaries             using ( _⟢_ )
open import Overture.Func.Inverses                  using ( eq )
open import Overture.Func.Surjective                using ( IsSurjective )
open import Relations.Func.Discrete                 using ( fkerPred )
open import Algebras.Func.Basic             {𝑆 = 𝑆} using ( SetoidAlgebra ; ov ; Lift-Alg )
open import Homomorphisms.Func.Basic        {𝑆 = 𝑆} using ( epi ; IsEpi ; IsHom ; hom ; epiβ†’hom )
open import Homomorphisms.Func.Properties   {𝑆 = 𝑆} using ( ∘-epi ; ToLift-epi )
open import Terms.Basic                     {𝑆 = 𝑆} using ( β„Š )
open import Terms.Func.Basic                {𝑆 = 𝑆} using ( 𝑻 ; _≐_ ; module Environment )
open import Terms.Func.Properties           {𝑆 = 𝑆} using ( free-lift )
open import Terms.Func.Operations           {𝑆 = 𝑆} using ( free-lift-interp )
open import Varieties.Func.SoundAndComplete {𝑆 = 𝑆} using ( Eq ; _⊫_ ; _β‰ˆΜ‡_ ; _⊒_β–Ή_β‰ˆ_
                                                          ; module Soundness
                                                          ; module FreeAlgebra
                                                          ; Th ; Mod )
open import Varieties.Func.Closure          {𝑆 = 𝑆} using ( V ; S )
open import Varieties.Func.Preservation     {𝑆 = 𝑆} using ( classIds-βŠ†-VIds ; S-id1 )

open Func using ( cong ) renaming ( f to _⟨$⟩_ )
open SetoidAlgebra using ( Domain )

In the code below, X will play the role of an arbitrary collection of variables; it would suffice to take X to be the cardinality of the largest algebra in 𝒦, but since we don’t know that cardinality, we leave X aribtrary for now.

Alternatively, we could let X be the product of all algebras in the class 𝒦, like so.

𝕏 : Type oΞ±
𝕏 = Carrier ( Domain (β¨… (𝔄{𝒦 = S 𝒦})) )

module FreeHom (Ο‡ : Level){Ξ± ρᡃ β„“ : Level}
               {𝒦 : Pred(SetoidAlgebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
 private
  ΞΉ = ov(Ο‡ βŠ” Ξ± βŠ” ρᡃ βŠ” β„“)

 open Eq

We now define the algebra 𝔽, which plays the role of the relatively free algebra, along with the natural epimorphism epi𝔽 : epi (𝑻 𝕏) 𝔽 from 𝑻 𝕏 to 𝔽. The relatively free algebra (relative to Th 𝒦) is called M and is derived from TermSetoid 𝕏 and TermInterp 𝕏 and imported from the EquationalLogic module.

 -- ℐ indexes the collection of equations modeled by 𝒦
 ℐ : Type ΞΉ
 ℐ = Ξ£[ eq ∈ Eq{Ο‡} ] 𝒦 ⊫ ((lhs eq) β‰ˆΜ‡ (rhs eq))

 β„° : ℐ β†’ Eq
 β„° (eqv , p) = eqv

 β„°βŠ’[_]β–ΉTh𝒦 : (X : Type Ο‡) β†’ βˆ€{p q} β†’ β„° ⊒ X β–Ή p β‰ˆ q β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 β„°βŠ’[ X ]β–ΉTh𝒦 x 𝑨 kA = sound (Ξ» i ρ β†’ βˆ₯ i βˆ₯ 𝑨 kA ρ) x
  where open Soundness β„° 𝑨

 ----------- THE RELATIVELY FREE ALGEBRA -----------
 open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )

Next we define an epimorphism from 𝑻 X onto the relatively free algebra 𝔽[ X ]. Of course, the kernel of this epimorphism will be the congruence of 𝑻 X defined by identities modeled by (S 𝒦, hence) 𝒦.

 epi𝔽[_] : (X : Type Ο‡) β†’ epi (𝑻 X) 𝔽[ X ]
 epi𝔽[ X ] = h , hepi
  where
  open SetoidAlgebra 𝔽[ X ] using () renaming ( Domain to F ; Interp to InterpF )
  open Setoid F using () renaming ( _β‰ˆ_  to _β‰ˆFβ‰ˆ_ ; refl to reflF )

  open SetoidAlgebra (𝑻 X) using () renaming (Domain to TX)
  open Setoid TX using () renaming ( _β‰ˆ_ to _β‰ˆTβ‰ˆ_ ; refl to reflT )


  open _≐_ ; open IsEpi ; open IsHom

  c : βˆ€ {x y} β†’ x β‰ˆTβ‰ˆ y β†’ x β‰ˆFβ‰ˆ y
  c (rfl {x}{y} ≑.refl) = reflF
  c (gnl {f}{s}{t} x) = cong InterpF (≑.refl , c ∘ x)

  h : TX ⟢ F
  h = record { f = id ; cong = c }

  hepi : IsEpi (𝑻 X) 𝔽[ X ] h
  compatible (isHom hepi) = cong h reflT
  isSurjective hepi {y} = eq y reflF


 hom𝔽[_] : (X : Type Ο‡) β†’ hom (𝑻 X) 𝔽[ X ]
 hom𝔽[ X ] = epiβ†’hom (𝑻 X) 𝔽[ X ] epi𝔽[ X ]

 hom𝔽[_]-is-epic : (X : Type Ο‡) β†’ IsSurjective ∣ hom𝔽[ X ] ∣
 hom𝔽[ X ]-is-epic = IsEpi.isSurjective (snd (epi𝔽[ X ]))


 class-models-kernel : βˆ€{X p q} β†’ (p , q) ∈ fkerPred ∣ hom𝔽[ X ] ∣ β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 class-models-kernel {X = X}{p}{q} pKq = β„°βŠ’[ X ]β–ΉTh𝒦 pKq

 kernel-in-theory : {X : Type Ο‡} β†’ fkerPred ∣ hom𝔽[ X ] ∣ βŠ† Th (V β„“ ΞΉ 𝒦)
 kernel-in-theory {X = X} {p , q} pKq vkA x = classIds-βŠ†-VIds {β„“ = β„“} {p = p}{q}
                                      (class-models-kernel pKq) vkA x


 module _  {X : Type Ο‡} {𝑨 : SetoidAlgebra Ξ± ρᡃ}{sA : 𝑨 ∈ S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦} where
  open Environment 𝑨 using ( Equal )
  kerπ”½βŠ†Equal : βˆ€{p q} β†’ (p , q) ∈ fkerPred ∣ hom𝔽[ X ] ∣ β†’ Equal p q
  kerπ”½βŠ†Equal{p = p}{q} x = S-id1{β„“ = β„“}{p = p}{q} (β„°βŠ’[ X ]β–ΉTh𝒦 x) 𝑨 sA


 π’¦βŠ«β†’β„°βŠ’ : {X : Type Ο‡} β†’ βˆ€{p q} β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ β„° ⊒ X β–Ή p β‰ˆ q
 π’¦βŠ«β†’β„°βŠ’ {p = p} {q} pKq = hyp ((p β‰ˆΜ‡ q) , pKq) where open _⊒_β–Ή_β‰ˆ_ using (hyp)


------------------------------------------------------------------------------

module _ {Ξ± ρᡃ β„“ : Level}
         {𝒦 : Pred(SetoidAlgebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
 private
  ΞΉ = ov(Ξ± βŠ” ρᡃ βŠ” β„“)

  open IsEpi ; open IsHom

 module lower-universe-version {𝑨 : SetoidAlgebra Ξ± ρᡃ} where
  open FreeHom Ξ± {Ξ±}{ρᡃ}{β„“}{𝒦}
  open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )
  open SetoidAlgebra 𝑨 using( Interp ) renaming (Domain to A)
  open Setoid A using ( trans ; sym ; refl ) renaming ( Carrier to ∣A∣ )

  𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] 𝑨
  𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
    where
    Ο† : (Domain 𝔽[ ∣A∣ ]) ⟢ A
    _⟨$⟩_ Ο† = free-lift{𝑨 = 𝑨} id
    cong Ο† {p} {q} pq =
     trans (sym (free-lift-interp{𝑨 = 𝑨} id p))
      (trans (A∈ModThK{p = p}{q} (kernel-in-theory pq) id)
      (free-lift-interp{𝑨 = 𝑨} id q))

    isEpi : IsEpi 𝔽[ ∣A∣ ] 𝑨 Ο†
    compatible (isHom isEpi) = cong Interp (≑.refl , (Ξ» _ β†’ refl))
    isSurjective isEpi {y} = eq (β„Š y) refl


  𝔽-ModTh-epi-lift : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦))
   β†’                 epi 𝔽[ ∣A∣ ] (Lift-Alg 𝑨 (ov Ξ±) (ov Ξ±))
  𝔽-ModTh-epi-lift A∈ModThK =
   ∘-epi (𝔽-ModTh-epi (Ξ» {p q} β†’ A∈ModThK{p = p}{q})) ToLift-epi


 module _ -- higher-universe-version
          -- (HSP theorem needs 𝑨 in higher universe level)
          {𝑨 : SetoidAlgebra (Ξ± βŠ” ρᡃ βŠ” β„“) (Ξ± βŠ” ρᡃ βŠ” β„“)} where

  open FreeHom (Ξ± βŠ” ρᡃ βŠ” β„“) {Ξ±}{ρᡃ}{β„“}{𝒦}
  open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )

  open SetoidAlgebra 𝑨 using( Interp ) renaming (Domain to A)
  open Setoid A using ( trans ; sym ; refl ) renaming ( Carrier to ∣A∣ )

  𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦))
   β†’            epi 𝔽[ ∣A∣ ] 𝑨
  𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
   where
   Ο† : (Domain 𝔽[ ∣A∣ ]) ⟢ A
   _⟨$⟩_ Ο† = free-lift{𝑨 = 𝑨} id
   cong Ο† {p} {q} pq = trans (sym (free-lift-interp{𝑨 = 𝑨} id p))
                      (trans (A∈ModThK{p = p}{q} (kernel-in-theory pq) id)
                      (free-lift-interp{𝑨 = 𝑨} id q))

   isEpi : IsEpi 𝔽[ ∣A∣ ] 𝑨 Ο†
   compatible (isHom isEpi) = cong Interp (≑.refl , (Ξ» _ β†’ refl))
   isSurjective isEpi {y} = eq (β„Š y) refl

  𝔽-ModTh-epi-lift : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] (Lift-Alg 𝑨 ΞΉ ΞΉ)
  𝔽-ModTh-epi-lift A∈ModThK =
   ∘-epi (𝔽-ModTh-epi (Ξ» {p q} β†’ A∈ModThK{p = p}{q})) ToLift-epi


← Varieties.Func.Closure Varieties.Func.HSP