---
layout: default
title : "Setoid.Varieties.Preservation (The Agda Universal Algebra Library)"
date : "2021-09-24"
author: "agda-algebras development team"
---

### 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 `𝒦`{.AgdaBound}, \af S `𝒦`{.AgdaBound}, \af P `𝒦`{.AgdaBound}, and \af V `𝒦`{.AgdaBound} all satisfy the
same identities.


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

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

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

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -------------------------------
open import Data.Product           using ( _,_ )
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 ; _βŠ†_ ; _∈_ )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture                                    using  ( proj₁ ; projβ‚‚ )

open import Overture.Terms                     {𝑆 = 𝑆}  using  ( Term )
open import Setoid.Algebras                    {𝑆 = 𝑆}  using  ( Algebra ; ov ; β¨… )
open import Setoid.Homomorphisms               {𝑆 = 𝑆}  using  ( ≅⨅⁺-refl ; β‰…-refl
                                                               ; IdHomImage ; β‰…-sym )
open import Setoid.Subalgebras                 {𝑆 = 𝑆}  using  ( _≀_ ; β¨…-≀ ; β‰…-trans-≀
                                                               ; ≀-reflexive )
open import Setoid.Terms                       {𝑆 = 𝑆}  using  ( module Environment)
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  ( _⊧_ ; _⊫_ ; ⊫-proof
                                                               ; _β‰ˆΜ‡_ ; _⊒_β–Ή_β‰ˆ_ ; Th)
open _⟢_      using () renaming ( to 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.

```agda
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 𝒦.

```agda
  PSβŠ†SP : P (a βŠ” β„“) oaβ„“ (S{Ξ² = Ξ±}{ρᡃ} β„“ 𝒦) βŠ† S oaβ„“ (P β„“ oaβ„“ 𝒦)
  PSβŠ†SP {𝑩} (I , ( π’œ , sA , Bβ‰…β¨…A )) = Goal
    where
    ℬ : I β†’ Algebra Ξ± ρᡃ
    ℬ i = sA i .proj₁

    kB : (i : I) β†’ ℬ i ∈ 𝒦
    kB i =  sA i .projβ‚‚ .proj₁

    β¨…A≀⨅B : β¨… π’œ ≀ β¨… ℬ
    β¨…A≀⨅B = β¨…-≀ Ξ» i β†’ projβ‚‚ (projβ‚‚ (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.

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

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

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

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

#### S preserves identities

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

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

#### P preserves identities

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

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

#### V preserves identities

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

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

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

  V-id1 : 𝒦 ⊫ (p β‰ˆΜ‡ q) β†’ V β„“ ΞΉ 𝒦 ⊫ (p β‰ˆΜ‡ q)
  V-id1 Οƒ .⊫-proof 𝑩 (𝑨 , (β¨…A , pβ¨…A , A≀⨅A) , BimgA) =
    H-id1{β„“ = aβ„“ΞΉ}{𝒦 = S aβ„“ΞΉ (P {Ξ² = Ξ±}{ρᡃ}β„“ ΞΉ 𝒦)} spK⊧pq .⊫-proof 𝑩 (𝑨 , (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-id1{β„“ = β„“} {𝒦 = 𝒦} Οƒ)

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

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

```agda
  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 = V-id2 Thpq
```