#### 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 Overture using (π ; π₯ ; Signature)

module Setoid.Varieties.Closure {π : 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 ( _Γ_ to _β§_ )
open import Data.Unit.Polymorphic  using ( β€ ; tt )
open import Function               using ( id ) 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       {π = π}  using ( Algebra ; ov ; Lift-Alg ; β¨ )
open  import Setoid.Homomorphisms  {π = π}
using ( IsHom ; _β_ ; β-trans ; β-sym ; Lift-β ; β¨ββ¨βΟ ; _IsHomImageOf_ )
using ( IdHomImage ; HomImage-β ; HomImage-β' ; Lift-HomImage-lemma )
open  import Setoid.Subalgebras    {π = π}
using ( _β€_ ; _β€c_ ; β€-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' : π© β€ lA'
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ββ¨π (β¨ββ¨βΟ{β = Ξ³}{Ο = ΟαΆ}))