 ### 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.

The next lemma would be too obvious to care about were it not for the fact that we’ll need it later, so it too must be formalized.

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

#### More class inclusions

We conclude this subsection with three more inclusion relations that will have bit parts to play later (e.g., in the formal proof of Birkhoff’s Theorem).

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