### Properties of the models relation

We prove some closure and invariance properties of the relation `β§`. In particular, we prove the following facts (which are needed, for example, in the proof the Birkhoff 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 Algebras.Basic using ( π ; π₯ ; Signature )

module Varieties.Properties {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive using ( _β_ ; lsuc ; Level )   renaming ( Set to Type ; lzero to  ββ )
open import Axiom.Extensionality.Propositional using ()   renaming ( Extensionality to funext )
open import Data.Product   using ( _,_ ; Ξ£-syntax ; _Γ_ ) renaming ( projβ to fst ; projβ to snd )
open import Function.Base  using ( _β_ )
open import Relation.Unary using ( Pred ; _β_ ; _β_ ; β )
open import Relation.Binary.PropositionalEquality using ( _β‘_ ; refl ; module β‘-Reasoning ; cong )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture.Preliminaries             using ( β£_β£ ; β₯_β₯ ; _β»ΒΉ )
open import Overture.Injective                 using ( IsInjective ; β-injective )
open import Equality.Welldefined               using ( SwellDef )
open import Equality.Extensionality            using ( DFunExt )
open import Algebras.Basic                     using ( Algebra ; Lift-Alg )
open import Algebras.Products          {π = π} using ( ov ; β¨ )
open import Homomorphisms.Basic        {π = π} using ( hom )
open import Homomorphisms.Properties   {π = π} using ( β-hom )
open import Homomorphisms.Isomorphisms {π = π} using ( _β_ ; mkiso ; Lift-β ; β-sym ; β-trans )
open import Terms.Basic                {π = π} using ( Term ; π» )
open import Terms.Properties           {π = π} using ( lift-hom )
open import Terms.Operations {π = π} using ( _β¦_β§ ; comm-hom-term ; interp-prod ; term-agreement )
open import Subalgebras.Subalgebras    {π = π} using ( _β€_ ; SubalgebraOfClass )
open import Subalgebras.Properties     {π = π} using ( isoβinjective )
open import Varieties.EquationalLogic  {π = π} using ( _β§_β_ ; _β«_β_ )

```

#### Algebraic invariance of β§

The binary relation β§ would be practically useless if it were not an algebraic invariant (i.e., 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                      β

```

As the proof makes clear, we show π© β§ 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 = β£ 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 π© π¨ (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) --  (β-sym Lift-β)

```

#### 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 β£ β β)     β

```