---
layout: default
title : "Setoid.Varieties.FreeAlgebras module (Agda Universal Algebra Library)"
date : "2021-06-29"
author: "agda-algebras development team"
---

#### Free setoid algebras


<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Varieties.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 ; _,_ )
open import Function         using ( _∘_ ; id )        renaming ( Func to _⟢_ )
open import Level            using ( Level ; _βŠ”_)
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( Pred ; _∈_ ; _βŠ†_ )

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  ( proj₁ ; projβ‚‚ )
open import Overture.Terms                     {𝑆 = 𝑆}  using  ( β„Š )
open import Setoid.Algebras                    {𝑆 = 𝑆}  using  ( Algebra ; ov ; Lift-Alg ; 𝔻[_] )
open import Setoid.Functions                            using  ( eq ; IsSurjective )
open import Setoid.Homomorphisms               {𝑆 = 𝑆}  using  ( epi ; IsEpi ; IsHom ; hom
                                                               ; epiβ†’hom ; βŠ™-epi ; ToLift-epi )
open import Setoid.Relations                            using  ( fkerPred )
open import Setoid.Terms                       {𝑆 = 𝑆}  using  ( 𝑻 ; _≐_ ; module Environment
                                                               ; free-lift ; free-lift-interp )
open import Setoid.Varieties.Closure           {𝑆 = 𝑆}  using  ( V ; S )

open import Setoid.Varieties.Preservation      {𝑆 = 𝑆}  using  ( classIds-βŠ†-VIds ; S-id1 )
open import Setoid.Varieties.SoundAndComplete  {𝑆 = 𝑆}  using  ( Eq ; _⊫_ ; ⊫-proof ; _β‰ˆΜ‡_ ; _⊒_β–Ή_β‰ˆ_
                                                               ; Th ; Mod ; module Soundness
                                                               ; module FreeAlgebra )
open _⟢_      using ( cong ) renaming ( to to _⟨$⟩_ )
open Algebra  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` arbitrary for now.

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

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

```agda
module FreeHom (Ο‡ : Level){Ξ± ρᡃ β„“ : Level}
               {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
  private
    ΞΉ : Level
    ΞΉ = 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.

```agda
 -- ℐ 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 .⊫-proof 𝑨 kA = sound (Ξ» i ρ β†’ (projβ‚‚ i) .⊫-proof 𝑨 kA ρ) x
    where open Soundness β„° 𝑨

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

Finally, 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) `𝒦`.

```agda
  epi𝔽[_] : (X : Type Ο‡) β†’ epi (𝑻 X) 𝔽[ X ]
  epi𝔽[ X ] = h , hepi
    where
    open Algebra 𝔽[ X ]  using() renaming ( Domain to F ; Interp to InterpF )
    open Setoid F        using() renaming ( _β‰ˆ_  to _β‰ˆFβ‰ˆ_ ; refl to reflF )
    open Algebra (𝑻 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 { to = 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 (proj₁ (hom𝔽[ X ]))
  hom𝔽[ X ]-is-epic = IsEpi.isSurjective (projβ‚‚ (epi𝔽[ X ]))


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

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


  module _  {X : Type Ο‡} {𝑨 : Algebra Ξ± ρᡃ}{sA : 𝑨 ∈ S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦} where
    open Environment 𝑨 using ( Equal )
    kerπ”½βŠ†Equal : βˆ€{p q} β†’ (p , q) ∈ fkerPred (proj₁ (hom𝔽[ X ])) β†’ Equal p q
    kerπ”½βŠ†Equal{p = p}{q} x = S-id1{β„“ = β„“} (β„°βŠ’[ X ]β–ΉTh𝒦 x) .⊫-proof 𝑨 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(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)} where
  private ΞΉ = ov(Ξ± βŠ” ρᡃ βŠ” β„“)
  open IsEpi ; open IsHom

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

    𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] 𝑨
    𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
      where
      Ο† : (Domain 𝔽[ ∣A∣ ]) ⟢ A
      Ο† ⟨$⟩ x = free-lift{𝑨 = 𝑨} id x
      Ο† .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∣ ] 𝑨 Ο†
      isEpi .isHom .compatible = cong Interp (≑.refl , Ξ» _ β†’ refl)
      isEpi .isSurjective = eq (β„Š _) 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 (needed by HSP theorem)
    {𝑨 : Algebra (Ξ± βŠ” ρᡃ βŠ” β„“) (Ξ± βŠ” ρᡃ βŠ” β„“)}
    where

    open FreeHom (Ξ± βŠ” ρᡃ βŠ” β„“) {Ξ±}{ρᡃ}{β„“}{𝒦}
    open FreeAlgebra {ΞΉ = ΞΉ}{I = ℐ} β„° using ( 𝔽[_] )
    open Algebra 𝑨 using( Interp ) renaming (Domain to A)
    open Environment 𝑨  using ( ⟦_⟧ )
    open Setoid A renaming ( Carrier to ∣A∣ )  using ( trans ; sym ; refl ; _β‰ˆ_)
    open SetoidReasoning A

    𝔽-ModTh-epi : 𝑨 ∈ Mod (Th (V β„“ ΞΉ 𝒦)) β†’ epi 𝔽[ ∣A∣ ] 𝑨
    𝔽-ModTh-epi A∈ModThK = Ο† , isEpi
      where
      Ο† : 𝔻[ 𝔽[ ∣A∣ ] ] ⟢ A
      Ο† ⟨$⟩ x = free-lift id x
      Ο† .cong {p} {q} pq = begin
          free-lift id p  β‰ˆΛ˜βŸ¨ free-lift-interp{𝑨 = 𝑨} id p ⟩
          ⟦ p ⟧ ⟨$⟩ id    β‰ˆβŸ¨ A∈ModThK{p = p}{q} (kernel-in-theory pq) id ⟩
          ⟦ q ⟧ ⟨$⟩ id    β‰ˆβŸ¨ free-lift-interp{𝑨 = 𝑨} id q ⟩
          free-lift id q  ∎

      isEpi : IsEpi 𝔽[ ∣A∣ ] 𝑨 Ο†
      isEpi .isHom .compatible = cong Interp (≑.refl , Ξ» _ β†’ refl)
      isEpi .isSurjective = eq (β„Š _) 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
```