↑ Top

Equation preservation for setoid algebras

This is the Setoid.Varieties.Preservation module of the Agda Universal Algebra Library where we show that the classes \af H \ab{𝒦}, \af S \ab{𝒦}, \af P \ab{𝒦}, and \af V \ab{𝒦} all satisfy the same identities.


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

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

module Setoid.Varieties.Preservation {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive         using ()       renaming ( Set to Type )
open import Data.Product           using ( _,_ )
                                   renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Data.Unit.Polymorphic  using ( ⊀ )
open import Function               using ( _∘_ )  renaming ( Func to _⟢_ )
open import Level                  using ( Level ; _βŠ”_ )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _βŠ†_ ; _∈_ )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Functions  using ( IsSurjective ; SurjInv ; SurjInvIsInverseΚ³ )

open import Base.Terms       {𝑆 = 𝑆} using ( Term )
open import Setoid.Algebras  {𝑆 = 𝑆} using ( Algebra ; ov ; π•Œ[_] ; Lift-Alg ; β¨… )

open  import Setoid.Homomorphisms {𝑆 = 𝑆}
      using ( ≅⨅⁺-refl ; β‰…-refl ; IdHomImage ; β‰…-sym )
open  import Setoid.Terms {𝑆 = 𝑆}
      using ( module Environment; comm-hom-term )
open  import Setoid.Subalgebras {𝑆 = 𝑆}
      using ( _≀_ ; _≀c_ ; β¨…-≀ ; β‰…-trans-≀ ; ≀-reflexive )
open  import Setoid.Varieties.Closure {𝑆 = 𝑆}
      using ( H ; S ; P ; S-expa ; H-expa ; V ; P-expa ; V-expa ;Level-closure )
open  import Setoid.Varieties.Properties {𝑆 = 𝑆}
      using ( ⊧-H-invar ; ⊧-S-invar ; ⊧-P-invar ; ⊧-I-invar )
open  import Setoid.Varieties.SoundAndComplete {𝑆 = 𝑆}
      using ( _⊧_ ; _⊨_ ; _⊫_ ; Eq ; _β‰ˆΜ‡_ ; lhs ; rhs ; _⊒_β–Ή_β‰ˆ_ ; Th)

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

Closure properties

The types defined above represent operators with useful closure properties. We now prove a handful of such properties that we need later.


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

 SβŠ†SP : βˆ€{ΞΉ} β†’ S β„“ 𝒦 βŠ† S {Ξ² = Ξ±}{ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦)
 SβŠ†SP {ΞΉ} (𝑨 , (kA , B≀A )) = 𝑨 , (pA , B≀A)
  where
  pA : 𝑨 ∈ P β„“ ΞΉ 𝒦
  pA = ⊀ , (Ξ» _ β†’ 𝑨) , (Ξ» _ β†’ kA) , ≅⨅⁺-refl

 PβŠ†SP : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 βŠ† S (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)
 PβŠ†SP {ΞΉ} x = S-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x


 PβŠ†HSP : βˆ€{ΞΉ} β†’  P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦
                 βŠ† H (a βŠ” β„“ βŠ” ΞΉ) (S {Ξ² = Ξ±}{ρᡃ}(a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦))
 PβŠ†HSP {ΞΉ} x = H-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ}  (S-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x)

 PβŠ†V : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 βŠ† V β„“ ΞΉ 𝒦
 PβŠ†V = PβŠ†HSP

 SPβŠ†V : βˆ€{ΞΉ} β†’ S{Ξ² = Ξ±}{ρᡇ = ρᡃ} (a βŠ” β„“ βŠ” ΞΉ) (P {Ξ² = Ξ±}{ρᡃ} β„“ ΞΉ 𝒦) βŠ† V β„“ ΞΉ 𝒦
 SPβŠ†V {ΞΉ} x = H-expa{β„“ = a βŠ” β„“ βŠ” ΞΉ} x

Finally, we are in a position to prove that a product of subalgebras of algebras in a class 𝒦 is a subalgebra of a product of algebras in 𝒦.


 PSβŠ†SP : P (a βŠ” β„“) oaβ„“ (S{Ξ² = Ξ±}{ρᡃ} β„“ 𝒦) βŠ† S oaβ„“ (P β„“ oaβ„“ 𝒦)
 PSβŠ†SP {𝑩} (I , ( π’œ , sA , Bβ‰…β¨…A )) = Goal
  where
  ℬ : I β†’ Algebra Ξ± ρᡃ
  ℬ i = ∣ sA i ∣
  kB : (i : I) β†’ ℬ i ∈ 𝒦
  kB i =  fst βˆ₯ sA i βˆ₯
  β¨…A≀⨅B : β¨… π’œ ≀ β¨… ℬ
  β¨…A≀⨅B = β¨…-≀ Ξ» i β†’ snd βˆ₯ sA i βˆ₯
  Goal : 𝑩 ∈ S{Ξ² = oaβ„“}{oaβ„“}oaβ„“ (P {Ξ² = oaβ„“}{oaβ„“} β„“ oaβ„“ 𝒦)
  Goal = β¨… ℬ , (I , (ℬ , (kB , β‰…-refl))) , (β‰…-trans-≀ Bβ‰…β¨…A β¨…A≀⨅B)

H preserves identities

First we prove that the closure operator H is compatible with identities that hold in the given class.


module _   {Ξ± ρᡃ β„“ Ο‡ : Level}
           {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)}
           {X : Type Ο‡}
           {p q : Term X}
           where

 H-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ H {Ξ² = Ξ±}{ρᡃ}β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 H-id1 Οƒ 𝑩 (𝑨 , kA , BimgA) = ⊧-H-invar{p = p}{q} (Οƒ 𝑨 kA) BimgA

The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.


 H-id2 : H β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 H-id2 Hpq 𝑨 kA = Hpq 𝑨 (𝑨 , (kA , IdHomImage))

S preserves identities


 S-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ (S {Ξ² = Ξ±}{ρᡃ} β„“ 𝒦) ⊫ (p β‰ˆΜ‡ q)
 S-id1 Οƒ 𝑩 (𝑨 , kA , B≀A) = ⊧-S-invar{p = p}{q} (Οƒ 𝑨 kA) B≀A

 S-id2 : S β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 S-id2 Spq 𝑨 kA = Spq 𝑨 (𝑨 , (kA , ≀-reflexive))

P preserves identities


 P-id1 : βˆ€{ΞΉ} β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 P-id1 Οƒ 𝑨 (I , π’œ , kA , Aβ‰…β¨…A) = ⊧-I-invar 𝑨 p q IH (β‰…-sym Aβ‰…β¨…A)
  where
  ih : βˆ€ i β†’ π’œ i ⊧ (p β‰ˆΜ‡ q)
  ih i = Οƒ (π’œ i) (kA i)
  IH : β¨… π’œ ⊧ (p β‰ˆΜ‡ q)
  IH = ⊧-P-invar {p = p}{q} π’œ ih

 P-id2 : βˆ€{ΞΉ} β†’ P β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 P-id2{ΞΉ} PKpq 𝑨 kA = PKpq 𝑨 (P-expa {β„“ = β„“}{ΞΉ} kA)

V preserves identities

Finally, we prove the analogous preservation lemmas for the closure operator V.


module _  {Ξ± ρᡃ β„“ ΞΉ Ο‡ : Level}
          {𝒦 : Pred(Algebra Ξ± ρᡃ) (Ξ± βŠ” ρᡃ βŠ” ov β„“)}
          {X : Type Ο‡}
          {p q : Term X} where

 private aβ„“ΞΉ = Ξ± βŠ” ρᡃ βŠ” β„“ βŠ” ΞΉ

 V-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ V β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 V-id1 Οƒ 𝑩 (𝑨 , (β¨…A , pβ¨…A , A≀⨅A) , BimgA) =
  H-id1{β„“ = aβ„“ΞΉ}{𝒦 = S aβ„“ΞΉ (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)}{p = p}{q} spK⊧pq 𝑩 (𝑨 , (spA , BimgA))
   where
   spA : 𝑨 ∈ S aβ„“ΞΉ (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)
   spA = β¨…A , (pβ¨…A , A≀⨅A)
   spK⊧pq : S aβ„“ΞΉ (P β„“ ΞΉ 𝒦) ⊫ (p β‰ˆΜ‡ q)
   spK⊧pq = S-id1{β„“ = aβ„“ΞΉ}{p = p}{q} (P-id1{β„“ = β„“} {𝒦 = 𝒦}{p = p}{q} Οƒ)

 V-id2 : V β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 V-id2 Vpq 𝑨 kA = Vpq 𝑨 (V-expa β„“ ΞΉ kA)

 Lift-id1 : βˆ€{Ξ² ρᡇ} β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ Level-closure{Ξ±}{ρᡃ}{Ξ²}{ρᡇ} β„“ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 Lift-id1 pKq 𝑨 (𝑩 , kB , Bβ‰…A) ρ = Goal
  where
  open Environment 𝑨
  open Setoid (Domain 𝑨) using (_β‰ˆ_)
  Goal : ⟦ p ⟧ ⟨$⟩ ρ β‰ˆ ⟦ q ⟧ ⟨$⟩ ρ
  Goal = ⊧-I-invar 𝑨 p q (pKq 𝑩 kB) Bβ‰…A ρ

Class identities

From V-id1 it follows that if 𝒦 is a class of structures, then the set of identities modeled by all structures in 𝒦 is equivalent to the set of identities modeled by all structures in V 𝒦. In other terms, Th (V 𝒦) is precisely the set of identities modeled by 𝒦. We formalize this observation as follows.


 classIds-βŠ†-VIds : 𝒦 ⊫ (p β‰ˆΜ‡ q)  β†’ (p , q) ∈ Th (V β„“ ΞΉ 𝒦)
 classIds-βŠ†-VIds pKq 𝑨 = V-id1 pKq 𝑨

 VIds-βŠ†-classIds : (p , q) ∈ Th (V β„“ ΞΉ 𝒦) β†’ 𝒦 ⊫ (p β‰ˆΜ‡ q)
 VIds-βŠ†-classIds Thpq 𝑨 kA = V-id2 Thpq 𝑨 kA

← Setoid.Varieties.Properties Setoid.Varieties.FreeAlgebras β†’