 ### Properties of the models relation

We prove some closure and invariance properties of the relation `⊧`. In particular, we prove the following facts (which we use later in our proof of Birkhoff’s HSP Theorem).

• Algebraic invariance. `⊧` is an algebraic invariant (stable under isomorphism).

• Subalgebraic invariance. Identities modeled by a class of algebras are also modeled by all subalgebras of algebras in the class.

• Product invariance. Identities modeled by a class of algebras are also modeled by all products of algebras in the class.

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

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Base.Varieties.Properties {𝑆 : 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 ; _×_ )
renaming ( proj₁ to fst ; proj₂ to snd )
open import Function        using ( _∘_ )
open import Level           using ( Level ; _⊔_ )
open import Relation.Unary  using ( Pred ; _∈_ ; _⊆_ ; ⋂ )
open import Axiom.Extensionality.Propositional
using () renaming ( Extensionality to funext )
open import Relation.Binary.PropositionalEquality
using ( _≡_ ; refl ; module ≡-Reasoning ; cong )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture                     using ( ∣_∣ ; ∥_∥ ; _⁻¹ )
open import Base.Functions               using ( IsInjective ; ∘-injective )
open import Base.Equality                using ( SwellDef ; DFunExt )
open import Base.Algebras       {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; ov ; ⨅ )
open import Base.Homomorphisms  {𝑆 = 𝑆}  using ( hom ; ∘-hom ; _≅_ ; mkiso )
using ( Lift-≅ ; ≅-sym ; ≅-trans )
open import Base.Terms          {𝑆 = 𝑆}  using ( Term ; 𝑻 ; lift-hom ; _⟦_⟧ )
using ( comm-hom-term ; interp-prod )
using ( term-agreement )
open import Base.Subalgebras    {𝑆 = 𝑆}  using ( _≤_ ; SubalgebraOfClass )
using ( iso→injective )
open import Base.Varieties.EquationalLogic
{𝑆 = 𝑆}  using ( _⊧_≈_ ; _⊫_≈_ )
```

#### Algebraic invariance of ⊧

The binary relation ⊧ would be practically useless if it were not an algebraic invariant (invariant under isomorphism).

```open Term
open ≡-Reasoning
open _≅_

module _  (wd : SwellDef){α β χ : Level}{X : Type χ}{𝑨 : Algebra α 𝑆}
(𝑩 : Algebra β 𝑆)(p q : Term X) where

⊧-I-invar : 𝑨 ⊧ p ≈ q  →  𝑨 ≅ 𝑩  →  𝑩 ⊧ p ≈ q

⊧-I-invar Apq (mkiso f g f∼g g∼f) x =
(𝑩 ⟦ p ⟧) x                       ≡⟨ wd χ β (𝑩 ⟦ p ⟧) x (∣ f ∣ ∘ ∣ g ∣ ∘ x) (λ i → ( f∼g (x i))⁻¹) ⟩
(𝑩 ⟦ p ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘ x)   ≡⟨ (comm-hom-term (wd 𝓥 β) 𝑩 f p (∣ g ∣ ∘ x))⁻¹ ⟩
∣ f ∣ ((𝑨 ⟦ p ⟧) (∣ g ∣ ∘ x))     ≡⟨ cong ∣ f ∣ (Apq (∣ g ∣ ∘ x))  ⟩
∣ f ∣ ((𝑨 ⟦ q ⟧) (∣ g ∣ ∘ x))     ≡⟨ comm-hom-term (wd 𝓥 β) 𝑩 f q (∣ g ∣ ∘ x) ⟩
(𝑩 ⟦ q ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘  x)  ≡⟨ wd χ β (𝑩 ⟦ q ⟧) (∣ f ∣ ∘ ∣ g ∣ ∘ x) x (λ i → ( f∼g (x i))) ⟩
(𝑩 ⟦ q ⟧) x                       ∎

```

In the above proof we showed `𝑩 ⊧ p ≈ q` by showing that `𝑩 ⟦ p ⟧ ≡ 𝑩 ⟦ q ⟧` holds extensionally, that is, `∀ x, 𝑩 ⟦ p ⟧ x ≡ 𝑩 ⟦q ⟧ x`.

#### Lift-invariance of ⊧

The `⊧` relation is also invariant under the algebraic lift and lower operations.

```module _ (wd : SwellDef){α β χ : Level}{X : Type χ}{𝑨 : Algebra α 𝑆} where

⊧-Lift-invar : (p q : Term X) → 𝑨 ⊧ p ≈ q → Lift-Alg 𝑨 β ⊧ p ≈ q
⊧-Lift-invar p q Apq = ⊧-I-invar wd (Lift-Alg 𝑨 _) p q Apq Lift-≅

⊧-lower-invar : (p q : Term X) → Lift-Alg 𝑨 β ⊧ p ≈ q  →  𝑨 ⊧ p ≈ q
⊧-lower-invar p q lApq = ⊧-I-invar wd 𝑨 p q lApq (≅-sym Lift-≅)
```

#### Subalgebraic invariance of ⊧

Identities modeled by an algebra `𝑨` are also modeled by every subalgebra of `𝑨`, which fact can be formalized as follows.

```module _ (wd : SwellDef){χ : Level}{𝓤 𝓦 : Level}{X : Type χ} where

⊧-S-invar : {𝑨 : Algebra 𝓤 𝑆}(𝑩 : Algebra 𝓦 𝑆){p q : Term X}
→          𝑨 ⊧ p ≈ q  →  𝑩 ≤ 𝑨  →  𝑩 ⊧ p ≈ q
⊧-S-invar {𝑨} 𝑩 {p}{q} Apq B≤A b = (∥ B≤A ∥) (ξ b)
where
h : hom 𝑩 𝑨
h = ∣ B≤A ∣

ξ : ∀ b → ∣ h ∣ ((𝑩 ⟦ p ⟧) b) ≡ ∣ h ∣ ((𝑩 ⟦ q ⟧) b)
ξ b =  ∣ h ∣((𝑩 ⟦ p ⟧) b)    ≡⟨ comm-hom-term (wd 𝓥 𝓤) 𝑨 h p b ⟩
(𝑨 ⟦ p ⟧)(∣ h ∣ ∘ b)  ≡⟨ Apq (∣ h ∣ ∘ b) ⟩
(𝑨 ⟦ q ⟧)(∣ h ∣ ∘ b)  ≡⟨ (comm-hom-term (wd 𝓥 𝓤) 𝑨 h q b)⁻¹ ⟩
∣ h ∣((𝑩 ⟦ q ⟧) b)    ∎

```

Next, identities modeled by a class of algebras is also modeled by all subalgebras of the class. In other terms, every term equation `p ≈ q` that is satisfied by all `𝑨 ∈ 𝒦` is also satisfied by every subalgebra of a member of `𝒦`.

``` ⊧-S-class-invar :  {𝒦 : Pred (Algebra 𝓤 𝑆)(ov 𝓤)}(p q : Term X)
→                 𝒦 ⊫ p ≈ q → (𝑩 : SubalgebraOfClass 𝒦) → ∣ 𝑩 ∣ ⊧ p ≈ q

⊧-S-class-invar p q Kpq (𝑩 , 𝑨 , SA , (ka , B≅SA)) =
⊧-S-invar 𝑩 {p}{q}((Kpq ka)) (h , hinj)
where
h : hom 𝑩 𝑨
h = ∘-hom 𝑩 𝑨 (to B≅SA) ∣ snd SA ∣
hinj : IsInjective ∣ h ∣
hinj = ∘-injective (iso→injective B≅SA) ∥ snd SA ∥
```

#### Product invariance of ⊧

An identity satisfied by all algebras in an indexed collection is also satisfied by the product of algebras in that collection.

```module _  (fe : DFunExt)(wd : SwellDef)
{α β χ : Level}{I : Type β}
(𝒜 : I → Algebra α 𝑆){X : Type χ} where

⊧-P-invar : (p q : Term X) → (∀ i → 𝒜 i ⊧ p ≈ q) → ⨅ 𝒜 ⊧ p ≈ q
⊧-P-invar p q 𝒜pq a = goal
where
-- This is where function extensionality is used.
ξ : (λ i → (𝒜 i ⟦ p ⟧) (λ x → (a x) i)) ≡ (λ i → (𝒜 i ⟦ q ⟧)  (λ x → (a x) i))
ξ = fe β α λ i → 𝒜pq i (λ x → (a x) i)

goal : (⨅ 𝒜 ⟦ p ⟧) a  ≡  (⨅ 𝒜 ⟦ q ⟧) a
goal =  (⨅ 𝒜 ⟦ p ⟧) a                      ≡⟨ interp-prod (wd 𝓥 (α ⊔ β)) p 𝒜 a ⟩
(λ i → (𝒜 i ⟦ p ⟧)(λ x → (a x)i))  ≡⟨ ξ ⟩
(λ i → (𝒜 i ⟦ q ⟧)(λ x → (a x)i))  ≡⟨ (interp-prod (wd 𝓥 (α ⊔ β)) q 𝒜 a)⁻¹ ⟩
(⨅ 𝒜 ⟦ q ⟧) a                      ∎

```

An identity satisfied by all algebras in a class is also satisfied by the product of algebras in the class.

``` ⊧-P-class-invar :  (𝒦 : Pred (Algebra α 𝑆)(ov α)){p q : Term X}
→                 𝒦 ⊫ p ≈ q → (∀ i → 𝒜 i ∈ 𝒦) → ⨅ 𝒜 ⊧ p ≈ q

⊧-P-class-invar 𝒦 {p}{q}σ K𝒜 = ⊧-P-invar p q λ i → σ (K𝒜 i)

```

Another fact that will turn out to be useful is that a product of a collection of algebras models `p ≈ q` if the lift of each algebra in the collection models `p ≈ q`.

``` ⊧-P-lift-invar : (p q : Term X) → (∀ i → Lift-Alg (𝒜 i) β ⊧ p ≈ q)  →  ⨅ 𝒜 ⊧ p ≈ q
⊧-P-lift-invar p q α = ⊧-P-invar p q Aipq
where
Aipq : ∀ i → (𝒜 i) ⊧ p ≈ q
Aipq i = ⊧-lower-invar wd p q (α i)
```

#### Homomorphic invariance of ⊧

If an algebra `𝑨` models an identity `p ≈ q`, then the pair `(p , q)` belongs to the kernel of every homomorphism `φ : hom (𝑻 X) 𝑨` from the term algebra to `𝑨`; that is, every homomorphism from `𝑻 X` to `𝑨` maps `p` and `q` to the same element of `𝑨`.

```module _ (wd : SwellDef){α χ : Level}{X : Type χ}{𝑨 : Algebra α 𝑆} where

⊧-H-invar : {p q : Term X}(φ : hom (𝑻 X) 𝑨) → 𝑨 ⊧ p ≈ q  →  ∣ φ ∣ p ≡ ∣ φ ∣ q

⊧-H-invar {p}{q}φ β =  ∣ φ ∣ p                ≡⟨ cong ∣ φ ∣(term-agreement(wd 𝓥 (ov χ)) p)⟩
∣ φ ∣((𝑻 X ⟦ p ⟧) ℊ)   ≡⟨ comm-hom-term (wd 𝓥 α) 𝑨 φ p ℊ ⟩
(𝑨 ⟦ p ⟧) (∣ φ ∣ ∘ ℊ)  ≡⟨ β (∣ φ ∣ ∘ ℊ ) ⟩
(𝑨 ⟦ q ⟧) (∣ φ ∣ ∘ ℊ)  ≡⟨ (comm-hom-term (wd 𝓥 α)  𝑨 φ q ℊ )⁻¹ ⟩
∣ φ ∣ ((𝑻 X ⟦ q ⟧) ℊ)  ≡⟨(cong ∣ φ ∣ (term-agreement (wd 𝓥 (ov χ)) q))⁻¹ ⟩
∣ φ ∣ q                ∎

```

More generally, an identity is satisfied by all algebras in a class if and only if that identity is invariant under all homomorphisms from the term algebra `𝑻 X` into algebras of the class. More precisely, if `𝒦` is a class of `𝑆`-algebras and `𝑝`, `𝑞` terms in the language of `𝑆`, then,

``````  𝒦 ⊧ p ≈ q  ⇔  ∀ 𝑨 ∈ 𝒦,  ∀ φ : hom (𝑻 X) 𝑨,  φ ∘ (𝑻 X)⟦ p ⟧ = φ ∘ (𝑻 X)⟦ q ⟧.
``````
```module _ (wd : SwellDef){α χ : Level}{X : Type χ}{𝒦 : Pred (Algebra α 𝑆)(ov α)}  where

-- ⇒ (the "only if" direction)
⊧-H-class-invar :  {p q : Term X}
→                 𝒦 ⊫ p ≈ q → ∀ 𝑨 φ → 𝑨 ∈ 𝒦 → ∀ a
→                 ∣ φ ∣ ((𝑻 X ⟦ p ⟧) a) ≡ ∣ φ ∣ ((𝑻 X ⟦ q ⟧) a)

⊧-H-class-invar {p = p}{q} σ 𝑨 φ ka a = ξ
where
ξ : ∣ φ ∣ ((𝑻 X ⟦ p ⟧) a) ≡ ∣ φ ∣ ((𝑻 X ⟦ q ⟧) a)
ξ =  ∣ φ ∣ ((𝑻 X ⟦ p ⟧) a)  ≡⟨ comm-hom-term (wd 𝓥 α) 𝑨 φ p a ⟩
(𝑨 ⟦ p ⟧)(∣ φ ∣ ∘ a)   ≡⟨ (σ ka) (∣ φ ∣ ∘ a) ⟩
(𝑨 ⟦ q ⟧)(∣ φ ∣ ∘ a)   ≡⟨ (comm-hom-term (wd 𝓥 α) 𝑨 φ q a)⁻¹ ⟩
∣ φ ∣ ((𝑻 X ⟦ q ⟧) a)  ∎

-- ⇐ (the "if" direction)
⊧-H-class-coinvar :  {p q : Term X}
→                   (∀ 𝑨 φ → 𝑨 ∈ 𝒦 → ∀ a → ∣ φ ∣ ((𝑻 X ⟦ p ⟧) a) ≡ ∣ φ ∣ ((𝑻 X ⟦ q ⟧) a))
→                   𝒦 ⊫ p ≈ q

⊧-H-class-coinvar {p}{q} β {𝑨} ka = goal
where
φ : (a : X → ∣ 𝑨 ∣) → hom (𝑻 X) 𝑨
φ a = lift-hom 𝑨 a

goal : 𝑨 ⊧ p ≈ q
goal a =  (𝑨 ⟦ p ⟧)(∣ φ a ∣ ∘ ℊ)     ≡⟨(comm-hom-term (wd 𝓥 α) 𝑨 (φ a) p ℊ)⁻¹ ⟩
(∣ φ a ∣ ∘ (𝑻 X ⟦ p ⟧)) ℊ  ≡⟨ β 𝑨 (φ a) ka ℊ ⟩
(∣ φ a ∣ ∘ (𝑻 X ⟦ q ⟧)) ℊ  ≡⟨ (comm-hom-term (wd 𝓥 α) 𝑨 (φ a) q ℊ) ⟩
(𝑨 ⟦ q ⟧)(∣ φ a ∣ ∘ ℊ)     ∎
```