---
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][].

This module proves that the classes `H`{.AgdaFunction}` 𝒦`{.AgdaBound},
`S`{.AgdaFunction}` 𝒦`{.AgdaBound},  `P`{.AgdaFunction}` 𝒦`{.AgdaBound}, and
`V`{.AgdaFunction}` 𝒦`{.AgdaBound} all satisfy the same identities.

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

module Setoid.Varieties.Preservation where

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

-- Imports from the Agda Standard Library -------------------------------
open import Data.Product           using ( _,_ ; proj₁ ; projβ‚‚ )
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  ( 𝑆 )
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 ; V ; S-expa ; H-expa
                                                      ; 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

Identities are inherited by subalgebras, so a class and its subalgebra closure
satisfy the same equations.  `S-id1`{.AgdaFunction} is the substantive direction
and is immediate from `⊧-S-invar`{.AgdaFunction} of
[Setoid.Varieties.Properties][]: an identity true in `𝑨` is true in anything
embedded in `𝑨`.  `S-id2`{.AgdaFunction} is the converse, and holds for the same
reason `H-id2`{.AgdaFunction} above does, namely that `S`{.AgdaFunction} is
expansive: `𝒦 βŠ† S β„“ 𝒦` by `≀-reflexive`{.AgdaFunction}, so an identity holding
throughout the closure holds in particular on `𝒦`.

```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

The same for products, with one extra step.  `P-id1`{.AgdaFunction} combines
`⊧-P-invar`{.AgdaFunction}, that a product of models is a model, with
`⊧-I-invar`{.AgdaFunction}, that satisfaction transports across an isomorphism.
The second is needed because membership in `P β„“ ΞΉ 𝒦` holds only *up to*
isomorphism: an inhabitant supplies a family `π’œ` together with a proof
`𝑨 β‰… β¨… π’œ`, not an equality.  `P-id2`{.AgdaFunction} is once more the
expansiveness converse, this time by way of `P-expa`{.AgdaFunction}.

```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
```