---
layout: default
title : "Legacy.Base.Varieties.Properties module (The Agda Universal Algebra Library)"
date : "2021-06-24"
author: "agda-algebras development team"
---

### <a id="properties-of-the-models-relation">Properties of the models relation</a>

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](#algebraic-invariance-of-models). `⊧` is an *algebraic invariant*
   (stable under isomorphism).

*  [Subalgebraic invariance](#subalgebraic-invariance). Identities modeled by a
   class of algebras are also modeled by all subalgebras of algebras in the class.

*  [Product invariance](#product-invariance-of-models). Identities modeled by a class of
   algebras are also modeled by all products of algebras in the class.


```agda


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

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

module Legacy.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 Legacy.Base.Functions               using ( IsInjective ; ∘-injective )
open import Legacy.Base.Equality                using ( SwellDef ; DFunExt )
open import Legacy.Base.Algebras       {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; ov ; β¨… )
open import Legacy.Base.Homomorphisms  {𝑆 = 𝑆}  using ( hom ; ∘-hom ; _β‰…_ ; mkiso )
                                         using ( Lift-β‰… ; β‰…-sym ; β‰…-trans )
open import Legacy.Base.Terms          {𝑆 = 𝑆}  using ( Term ; 𝑻 ; lift-hom ; _⟦_⟧ )
                                         using ( comm-hom-term ; interp-prod )
                                         using ( term-agreement )
open import Legacy.Base.Subalgebras    {𝑆 = 𝑆}  using ( _≀_ ; SubalgebraOfClass )
                                         using ( iso→injective )
open import Legacy.Base.Varieties.EquationalLogic
                                {𝑆 = 𝑆}  using ( _⊧_β‰ˆ_ ; _⊫_β‰ˆ_ )
```



#### <a id="algebraic-invariance-of-models">Algebraic invariance of ⊧</a>

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


```agda


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                       β‰‘βŸ¨ i p ⟩
  (𝑩 ⟦ p ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘ x)   β‰‘βŸ¨ (ii p) ⁻¹ ⟩
  ∣ f ∣ ((𝑨 ⟦ p ⟧) (∣ g ∣ ∘ x))     β‰‘βŸ¨ cong ∣ f ∣ (Apq (∣ g ∣ ∘ x))  ⟩
  ∣ f ∣ ((𝑨 ⟦ q ⟧) (∣ g ∣ ∘ x))     β‰‘βŸ¨ ii q ⟩
  (𝑩 ⟦ q ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘  x)  β‰‘βŸ¨ (i q)⁻¹ ⟩
  (𝑩 ⟦ q ⟧) x                       ∎
  where
  i : βˆ€ t β†’ (𝑩 ⟦ t ⟧) x ≑ (𝑩 ⟦ t ⟧) Ξ» x₁ β†’ ∣ f ∣ (∣ g ∣ (x x₁))
  i t = wd Ο‡ Ξ² (𝑩 ⟦ t ⟧) x (∣ f ∣ ∘ ∣ g ∣ ∘ x) Ξ» i β†’ ( f∼g (x i))⁻¹

  ii :  βˆ€ t
   β†’    ∣ f ∣((𝑨 ⟦ t ⟧) Ξ» x₁ β†’ ∣ g ∣(x x₁)) ≑ (𝑩 ⟦ t ⟧) Ξ» x₁ β†’ ∣ f ∣(∣ g ∣(x x₁))
  ii t = comm-hom-term (wd π“₯ Ξ²) 𝑩 f t (∣ g ∣ ∘ x)
```



In the above proof we showed `𝑩 ⊧ p β‰ˆ q` by showing that `𝑩 ⟦ p ⟧ ≑ 𝑩 ⟦ q ⟧` holds
*extensionally*, that is, `βˆ€ x, 𝑩 ⟦ p ⟧ x ≑ 𝑩 ⟦q ⟧ x`.

#### <a id="lift-invariance-of-models">Lift-invariance of ⊧</a>
The `⊧` relation is also invariant under the algebraic lift and lower operations.


```agda


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-β‰…)
```




#### <a id="subalgebraic-invariance">Subalgebraic invariance of ⊧</a>

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


```agda


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

 
```agda


 ⊧-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 βˆ₯
```



#### <a id="product-invariance-of-models">Product invariance of ⊧</a>

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


```agda


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.


```agda


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


```agda


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


#### <a id="homomorphisc-invariance-of-models">Homomorphic invariance of ⊧</a>

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

 
```agda


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                β‰‘βŸ¨ i p ⟩
                        ∣ Ο† ∣((𝑻 X ⟦ p ⟧) β„Š)   β‰‘βŸ¨ ii p ⟩
                        (𝑨 ⟦ p ⟧) (∣ Ο† ∣ ∘ β„Š)  β‰‘βŸ¨ Ξ² (∣ Ο† ∣ ∘ β„Š ) ⟩
                        (𝑨 ⟦ q ⟧) (∣ Ο† ∣ ∘ β„Š)  β‰‘βŸ¨ (ii q)⁻¹ ⟩
                        ∣ Ο† ∣ ((𝑻 X ⟦ q ⟧) β„Š)  β‰‘βŸ¨ (i q)⁻¹ ⟩
                        ∣ Ο† ∣ q                ∎

  where
  i : βˆ€ t β†’ ∣ Ο† ∣ t ≑ ∣ Ο† ∣ ((𝑻 X ⟦ t ⟧) β„Š)
  i t = cong ∣ Ο† ∣(term-agreement(wd π“₯ (ov Ο‡)) t)
  ii : βˆ€ t β†’ ∣ Ο† ∣ ((𝑻 X ⟦ t ⟧) β„Š) ≑ (𝑨 ⟦ t ⟧) (Ξ» x β†’ ∣ Ο† ∣ (β„Š x))
  ii t = comm-hom-term (wd π“₯ Ξ±) 𝑨 Ο† t β„Š
```


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

```agda


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 ∣ ∘ β„Š)     ∎
```