#### Closure Operators for Setoid Algebras

Fix a signature π, let π¦ be a class of π-algebras, and define

• H π¦ = algebras isomorphic to a homomorphic image of a members of π¦;
• S π¦ = algebras isomorphic to a subalgebra of a member of π¦;
• P π¦ = algebras isomorphic to a product of members of π¦.
```{-# OPTIONS --without-K --exact-split --safe #-}

open import Base.Algebras.Basic using ( π ; π₯ ; Signature )

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

-- imports from Agda and the Agda Standard Library -------------------------------------------
open import Agda.Primitive         using ( _β_ ; lsuc )      renaming ( Set to Type ; lzero to ββ)
open import Data.Product           using ( _,_ ; Ξ£-syntax )  renaming ( _Γ_ to _β§_ )
open import Data.Unit.Polymorphic  using ( β€ ; tt )
open import Function.Base          using ( id )
open import Function.Bundles       using ()                  renaming ( Func to _βΆ_ )
open import Level                  using ( Level ; Lift ; lift ; lower )
open import Relation.Binary        using ( Setoid )
open import Relation.Unary         using ( Pred ; _β_ ; _β_ )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Setoid.Algebras.Basic                   {π = π}  using ( Algebra ; ov ; Lift-Alg )
open import Setoid.Algebras.Products                {π = π}  using ( β¨ )
open import Setoid.Homomorphisms.Basic              {π = π}  using ( IsHom )
open import Setoid.Homomorphisms.Isomorphisms       {π = π}  using ( _β_ ; β-trans ; β-sym ; Lift-β ; β¨ββ¨βΟ )
open import Setoid.Homomorphisms.HomomorphicImages  {π = π}  using ( _IsHomImageOf_ ; IdHomImage ; HomImage-β )
using ( HomImage-β' ; Lift-HomImage-lemma )
open import Setoid.Subalgebras.Subalgebras          {π = π}  using ( _β€_ ; _β€c_ )
open import Setoid.Subalgebras.Properties           {π = π}  using ( β€-reflexive ; β€-trans ; β-trans-β€ )
using ( β€-trans-β ; Lift-β€-Lift ; β€-Lift )

open _βΆ_ renaming ( f to _β¨\$β©_ )

module _ {Ξ± Οα΅ Ξ² Οα΅ : Level} where

private a = Ξ± β Οα΅ ; b = Ξ² β Οα΅

Level-closure : β β β Pred(Algebra Ξ± Οα΅) (a β ov β) β Pred(Algebra Ξ² Οα΅) (b β ov(a β β))
Level-closure β π¦ π© = Ξ£[ π¨ β Algebra Ξ± Οα΅ ]  (π¨ β π¦)  β§  π¨ β π©

module _ {Ξ± Οα΅ Ξ² Οα΅ : Level} where

Lift-closed : β β β {π¦ : Pred(Algebra Ξ± Οα΅) _}{π¨ : Algebra Ξ± Οα΅} β π¨ β π¦
β            Lift-Alg π¨ Ξ² Οα΅ β (Level-closure β π¦)
Lift-closed _ {π¨ = π¨} kA = π¨ , (kA , Lift-β)

module _  {Ξ± Οα΅ Ξ² Οα΅ : Level} where

private a = Ξ± β Οα΅ ; b = Ξ² β Οα΅

H : β β β Pred(Algebra Ξ± Οα΅) (a β ov β) β Pred(Algebra Ξ² Οα΅) (b β ov(a β β))
H _ π¦ π© = Ξ£[ π¨ β Algebra Ξ± Οα΅ ] π¨ β π¦ β§ π© IsHomImageOf π¨

S : β β β Pred(Algebra Ξ± Οα΅) (a β ov β) β Pred(Algebra Ξ² Οα΅) (b β ov(a β β))
S _ π¦ π© = Ξ£[ π¨ β Algebra Ξ± Οα΅ ] π¨ β π¦ β§ π© β€ π¨

P : β β ΞΉ β Pred(Algebra Ξ± Οα΅) (a β ov β) β Pred(Algebra Ξ² Οα΅) (b β ov(a β β β ΞΉ))
P β ΞΉ π¦ π© = Ξ£[ I β Type ΞΉ ] (Ξ£[ π β (I β Algebra Ξ± Οα΅) ] (β i β π i β π¦) β§ (π© β β¨ π))

module _  {Ξ± Οα΅ Ξ² Οα΅ : Level} where

private a = Ξ± β Οα΅ ; b = Ξ² β Οα΅

SP : β β ΞΉ β Pred(Algebra Ξ± Οα΅) (a β ov β) β Pred(Algebra Ξ² Οα΅) (b β ov(a β β β ΞΉ))
SP β ΞΉ π¦ = S{Ξ±}{Οα΅} (a β β β ΞΉ) (P β ΞΉ π¦)

module _  {Ξ± Οα΅ Ξ² Οα΅ Ξ³ ΟαΆ Ξ΄ Οα΅ : Level} where

private a = Ξ± β Οα΅ ; b = Ξ² β Οα΅ ; c = Ξ³ β ΟαΆ ; d = Ξ΄ β Οα΅

V : β β ΞΉ β Pred(Algebra Ξ± Οα΅) (a β ov β) β  Pred(Algebra Ξ΄ Οα΅) (d β ov(a β b β c β β β ΞΉ))
V β ΞΉ π¦ = H{Ξ³}{ΟαΆ}{Ξ΄}{Οα΅} (a β b β β β ΞΉ) (S{Ξ²}{Οα΅} (a β β β ΞΉ) (P β ΞΉ π¦))

```

Thus, if π¦ is a class of π-algebras, then the variety generated by π¦ is denoted by `V π¦` and defined to be the smallest class that contains π¦ and is closed under `H`, `S`, and `P`.

With the closure operator V representing closure under HSP, we represent formally what it means to be a variety of algebras as follows.

```module _ {Ξ± Οα΅ β ΞΉ : Level} where

is-variety : (π± : Pred (Algebra Ξ± Οα΅)(Ξ± β Οα΅ β ov β)) β Type (ov (Ξ± β Οα΅ β β β ΞΉ))
is-variety π± = V{Ξ² = Ξ±}{Οα΅ = Οα΅}{Ξ³ = Ξ±}{ΟαΆ = Οα΅} β ΞΉ π± β π±

variety : Type (ov (Ξ± β Οα΅ β ov β β ΞΉ))
variety = Ξ£[ π± β (Pred (Algebra Ξ± Οα΅) (Ξ± β Οα΅ β ov β)) ] is-variety π±

```

#### Closure properties of S

`S` is a closure operator. The fact that S is expansive wonβt be needed, so we omit the proof, but we will make use of monotonicity and idempotence of `S`.

```module _ {Ξ± Οα΅ : Level} where

private a = Ξ± β Οα΅

S-mono : β{β} β {π¦ π¦' : Pred (Algebra Ξ± Οα΅)(a β ov β)}
β       π¦ β π¦' β S{Ξ² = Ξ±}{Οα΅} β π¦ β S β π¦'

S-mono kk {π©} (π¨ , (kA , Bβ€A)) = π¨ , ((kk kA) , Bβ€A)

```

We say `S` is idempotent provided \af{S} (\af{S} \ab{π¦}) \as{=} \af{S} \ab{π¦}. Of course, this is proved by establishing two inclusions, but one of them is trivial, so only the other need be formalized, which we do as follows.

``` S-idem : β{Ξ² Οα΅ Ξ³ ΟαΆ β} β {π¦ : Pred (Algebra Ξ± Οα΅)(a β ov β)}
β       S{Ξ² = Ξ³}{ΟαΆ} (a β β) (S{Ξ² = Ξ²}{Οα΅} β π¦) β S{Ξ² = Ξ³}{ΟαΆ} β π¦

S-idem (π¨ , (π© , sB , Aβ€B) , xβ€A) = π© , (sB , β€-trans xβ€A Aβ€B)

```

#### Closure properties of P

`P` is a closure operator. This is proved by checking that `P` is monotone, expansive, and idempotent. The meaning of these terms will be clear from the definitions of the types that follow.

``` H-expa : β{β} β {π¦ : Pred (Algebra Ξ± Οα΅)(a β ov β)} β π¦ β H β π¦
H-expa {β} {π¦}{π¨} kA = π¨ , kA , IdHomImage

S-expa : β{β} β {π¦ : Pred (Algebra Ξ± Οα΅)(a β ov β)} β π¦ β S β π¦
S-expa {β}{π¦}{π¨} kA = π¨ , (kA , β€-reflexive)

P-mono : β{β ΞΉ} β {π¦ π¦' : Pred (Algebra Ξ± Οα΅)(a β ov β)}
β       π¦ β π¦' β P{Ξ² = Ξ±}{Οα΅} β ΞΉ π¦ β P β ΞΉ π¦'

P-mono {β}{ΞΉ}{π¦}{π¦'} kk {π©} (I , π , (kA , Bββ¨A)) = I , (π , ((Ξ» i β kk (kA i)) , Bββ¨A))

open _β_
open IsHom

P-expa : β{β ΞΉ} β {π¦ : Pred (Algebra Ξ± Οα΅)(a β ov β)} β π¦ β P β ΞΉ π¦
P-expa {β}{ΞΉ}{π¦}{π¨} kA = β€ , (Ξ» x β π¨) , ((Ξ» i β kA) , Goal)
where
open Algebra π¨ using () renaming (Domain to A)
open Algebra (β¨ (Ξ» _ β π¨)) using () renaming (Domain to β¨A)
open Setoid A using ( refl )
open Setoid β¨A using () renaming ( refl to reflβ¨ )

toβ¨ : A βΆ β¨A
(toβ¨ β¨\$β© x) = Ξ» _ β x
cong toβ¨ xy = Ξ» _ β xy
toβ¨IsHom : IsHom π¨ (β¨ (Ξ» _ β π¨)) toβ¨
compatible toβ¨IsHom =  reflβ¨

fromβ¨ : β¨A βΆ A
(fromβ¨ β¨\$β© x) = x tt
cong fromβ¨ xy = xy tt
fromβ¨IsHom : IsHom (β¨ (Ξ» _ β π¨)) π¨ fromβ¨
compatible fromβ¨IsHom = refl

Goal : π¨ β β¨ (Ξ» x β π¨)
to Goal = toβ¨ , toβ¨IsHom
from Goal = fromβ¨ , fromβ¨IsHom
toβΌfrom Goal = Ξ» _ _ β refl
fromβΌto Goal = Ξ» _ β refl

V-expa : β β ΞΉ β {π¦ : Pred (Algebra Ξ± Οα΅)(a β ov β)} β π¦ β V β ΞΉ π¦
V-expa β ΞΉ {π¦} {π¨} x = H-expa {a β β β ΞΉ} (S-expa {a β β β ΞΉ} (P-expa {β}{ΞΉ} x) )

```

We sometimes want to go back and forth between our two representations of subalgebras of algebras in a class. The tools `subalgebraβS` and `Sβsubalgebra` are made for that purpose.

```module _ {Ξ± Οα΅ Ξ² Οα΅ β ΞΉ : Level}{π¦ : Pred (Algebra Ξ± Οα΅)(Ξ± β Οα΅ β ov β)}
{π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where

S-β : π¨ β S β π¦ β π¨ β π© β π© β S{Ξ± β Ξ²}{Οα΅ β Οα΅}(Ξ± β Οα΅ β β) (Level-closure β π¦)
S-β (π¨' , kA' , Aβ€A') AβB = lA' , (lklA' , Bβ€lA')
where
lA' : Algebra (Ξ± β Ξ²) (Οα΅ β Οα΅)
lA' = Lift-Alg π¨' Ξ² Οα΅
lklA' : lA' β Level-closure β π¦
lklA' = Lift-closed β kA'
subgoal : π¨ β€ lA'
subgoal = β€-trans-β Aβ€A' Lift-β
Bβ€lA' = β-trans-β€ (β-sym AβB) subgoal

V-β : π¨ β V β ΞΉ π¦ β π¨ β π© β π© β V{Ξ² = Ξ±}{Οα΅} β ΞΉ π¦
V-β (π¨' , spA' , AimgA') AβB = π¨' , spA' , HomImage-β AimgA' AβB

module _ {Ξ± Οα΅ β : Level}
(π¦ : Pred(Algebra Ξ± Οα΅) (Ξ± β Οα΅ β ov β))
(π¨ : Algebra (Ξ± β Οα΅ β β) (Ξ± β Οα΅ β β)) where

private ΞΉ = ov(Ξ± β Οα΅ β β)

V-β-lc : Lift-Alg π¨ ΞΉ ΞΉ β V{Ξ² = ΞΉ}{ΞΉ} β ΞΉ π¦
β       π¨ β V{Ξ³ = ΞΉ}{ΞΉ} β ΞΉ π¦

V-β-lc (π¨' , spA' , lAimgA') = π¨' , (spA' , AimgA')
where
AimgA' : π¨ IsHomImageOf π¨'
AimgA' = Lift-HomImage-lemma lAimgA'

```

The remaining theorems in this file are as yet unused, but may be useful later and/or for reference.

```module _ {Ξ± Οα΅ β ΞΉ : Level}{π¦ : Pred (Algebra Ξ± Οα΅)(Ξ± β Οα΅ β ov β)} where

-- For reference, some useful type levels:
classP : Pred (Algebra Ξ± Οα΅) (ov(Ξ± β Οα΅ β β β ΞΉ))
classP = P{Ξ² = Ξ±}{Οα΅} β ΞΉ π¦

classSP : Pred (Algebra Ξ± Οα΅) (ov(Ξ± β Οα΅ β β β ΞΉ))
classSP = S{Ξ² = Ξ±}{Οα΅} (Ξ± β Οα΅ β β β ΞΉ) (P{Ξ² = Ξ±}{Οα΅} β ΞΉ π¦)

classHSP : Pred (Algebra Ξ± Οα΅) (ov(Ξ± β Οα΅ β β β ΞΉ))
classHSP = H{Ξ² = Ξ±}{Οα΅}(Ξ± β Οα΅ β β β ΞΉ) (S{Ξ² = Ξ±}{Οα΅}(Ξ± β Οα΅ β β β ΞΉ) (P{Ξ² = Ξ±}{Οα΅}β ΞΉ π¦))

classS : β{Ξ² Οα΅} β Pred (Algebra Ξ² Οα΅) (Ξ² β Οα΅ β ov(Ξ± β Οα΅ β β))
classS = S β π¦
classK : β{Ξ² Οα΅} β Pred (Algebra Ξ² Οα΅) (Ξ² β Οα΅ β ov(Ξ± β Οα΅ β β))
classK = Level-closure{Ξ±}{Οα΅} β π¦

module _ {Ξ± Οα΅ Ξ² Οα΅ Ξ³ ΟαΆ β : Level}{π¦ : Pred (Algebra Ξ± Οα΅)(Ξ± β Οα΅ β ov β)} where
private a = Ξ± β Οα΅ ; b = Ξ² β Οα΅ ; c = Ξ³ β ΟαΆ

LevelClosure-S : Pred (Algebra (Ξ± β Ξ³) (Οα΅ β ΟαΆ)) (c β ov(a β b β β))
LevelClosure-S = Level-closure{Ξ²}{Οα΅} (a β β) (S β π¦)

S-LevelClosure : Pred (Algebra (Ξ± β Ξ³) (Οα΅ β ΟαΆ)) (ov(a β c β β))
S-LevelClosure = S{Ξ± β Ξ³}{Οα΅ β ΟαΆ}(a β β) (Level-closure β π¦)

S-Lift-lemma : LevelClosure-S β S-LevelClosure
S-Lift-lemma {πͺ} (π© , (π¨ , (kA , Bβ€A)) , BβC) = Lift-Alg π¨ Ξ³ ΟαΆ
, (Lift-closed{Ξ² = Ξ³}{ΟαΆ} β kA)
, Cβ€lA
where
Bβ€lA : π© β€ Lift-Alg π¨ Ξ³ ΟαΆ
Bβ€lA = β€-Lift Bβ€A
Cβ€lA : πͺ β€ Lift-Alg π¨ Ξ³ ΟαΆ
Cβ€lA = β-trans-β€ (β-sym BβC) Bβ€lA

module _ {Ξ± Οα΅ : Level} where

P-Lift-closed : β β ΞΉ β {π¦ : Pred (Algebra Ξ± Οα΅)(Ξ± β Οα΅ β ov β)}{π¨ : Algebra Ξ± Οα΅}
β              π¨ β P{Ξ² = Ξ±}{Οα΅} β ΞΉ π¦
β              {Ξ³ ΟαΆ : Level} β Lift-Alg π¨ Ξ³ ΟαΆ β P (Ξ± β Οα΅ β β) ΞΉ (Level-closure β π¦)
P-Lift-closed β ΞΉ {π¦}{π¨} (I , π , kA , Aββ¨π) {Ξ³}{ΟαΆ} = I
, (Ξ» x β Lift-Alg (π x) Ξ³ ΟαΆ)
, goal1 , goal2

where
goal1 : (i : I) β Lift-Alg (π i) Ξ³ ΟαΆ β Level-closure β π¦
goal1 i = Lift-closed β (kA i)
goal2 : Lift-Alg π¨ Ξ³ ΟαΆ β β¨ (Ξ» x β Lift-Alg (π x) Ξ³ ΟαΆ)
goal2 = β-trans (β-sym Lift-β) (β-trans Aββ¨π (β¨ββ¨βΟ{β = Ξ³}{Ο = ΟαΆ}))

```