Agda UALib β

### Subuniverses

This section presents the Subalgebras.Subuniverses module of the Agda Universal Algebra Library.

We start by defining a type that represents the important concept of subuniverse. Suppose π¨ is an algebra. A subset B β β£ π¨ β£ is said to be closed under the operations of π¨ if for each π β β£ π β£ and all tuples π : β₯ π β₯ π β π΅ the element (π Μ π¨) π belongs to B. If a subset B β π΄ is closed under the operations of π¨, then we call B a subuniverse of π¨.

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

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

module Subalgebras.Subuniverses {π : Signature π π₯} where

open import Terms.Operations{π = π} public
open import Relation.Unary using (β) public

```

We first show how to represent in Agda the collection of subuniverses of an algebra `π¨`. Since a subuniverse is viewed as a subset of the domain of `π¨`, we define it as a predicate on `β£ π¨ β£`. Thus, the collection of subuniverses is a predicate on predicates on `β£ π¨ β£`.

```
module _ {π€ π¦ : Universe} where

Subuniverses : (π¨ : Algebra π€ π) β Pred (Pred β£ π¨ β£ π¦)(π β π₯ β π€ β π¦)
Subuniverses π¨ B = (π : β£ π β£)(π : β₯ π β₯ π β β£ π¨ β£) β Im π β B β (π Μ π¨) π β B

```

Hereβs one way to construct an algebra out of a subuniverse.

```
SubunivAlg : (π¨ : Algebra π€ π)(B : Pred β£ π¨ β£ π¦) β B β Subuniverses π¨ β Algebra (π€ β π¦) π
SubunivAlg π¨ B BβSubA = Ξ£ B , Ξ» π π β (π Μ π¨)(fst β π) , BβSubA π (fst β π)(snd β π)

```

#### Subuniverses as records

Next we define a type to represent a single subuniverse of an algebra. If `π¨` is the algebra in question, then a subuniverse of `π¨` is a subset of (i.e., predicate over) the domain `β£ π¨ β£` that belongs to `Subuniverses π¨`.

```
record Subuniverse {π¨ : Algebra π€ π} : ov (π€ β π¦) Μ where
constructor mksub
field
sset  : Pred β£ π¨ β£ π¦
isSub : sset β Subuniverses π¨

```

#### Subuniverse Generation

If `π¨` is an algebra and `X β β£ π¨ β£` a subset of the domain of `π¨`, then the subuniverse of `π¨` generated by `X` is typically denoted by `Sg``π¨``(X)` and defined to be the smallest subuniverse of `π¨` containing `X`. Equivalently,

`Sg``π¨``(X)` = `β` { `U` : `U` is a subuniverse of `π¨` and `B β U` }.

We define an inductive type, denoted by `Sg`, that represents the subuniverse generated by a given subset of the domain of a given algebra, as follows.

```
data Sg (π¨ : Algebra π€ π)(X : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π¦ β π€) where
var : β {v} β v β X β v β Sg π¨ X
app : (π : β£ π β£)(π : β₯ π β₯ π β β£ π¨ β£) β Im π β Sg π¨ X β (π Μ π¨) π β Sg π¨ X

```

Given an arbitrary subset `X` of the domain `β£ π¨ β£` of an `π`-algebra `π¨`, the type `Sg X` does indeed represent a subuniverse of `π¨`. Proving this using the inductive type `Sg` is trivial, as we see here.

```
module _ {π€ π¦ : Universe} where

sgIsSub : {π¨ : Algebra π€ π}{X : Pred β£ π¨ β£ π¦} β Sg π¨ X β Subuniverses π¨
sgIsSub = app

```

Next we prove by structural induction that `Sg X` is the smallest subuniverse of `π¨` containing `X`.

```
sgIsSmallest : {π‘ : Universe}(π¨ : Algebra π€ π){X : Pred β£ π¨ β£ π¦}(Y : Pred β£ π¨ β£ π‘)
β             Y β Subuniverses π¨  β  X β Y  β  Sg π¨ X β Y

sgIsSmallest _ _ _ XinY (var Xv) = XinY Xv

sgIsSmallest π¨ Y YsubA XinY (app π π SgXa) = faβY
where
IH : Im π β Y
IH i = sgIsSmallest π¨ Y YsubA XinY (SgXa i)

faβY : (π Μ π¨) π β Y
faβY = YsubA π π IH

```

When the element of `Sg X` is constructed as `app π π SgXa`, we may assume (the induction hypothesis) that the arguments in the tuple `π` belong to `Y`. Then the result of applying `π` to `π` also belongs to `Y` since `Y` is a subuniverse.

#### Subuniverse Lemmas

Here we formalize a few basic properties of subuniverses. First, the intersection of subuniverses is again a subuniverse.

```
module _ {π π€ π¦ : Universe} where

sub-intersection : {π¨ : Algebra π€ π}{I : π Μ}{π : I β Pred β£ π¨ β£ π¦}
β                 Ξ  i κ I , π i β Subuniverses π¨
----------------------------------
β                 β I π β Subuniverses π¨

sub-intersection Ξ± π π Ξ² = Ξ» i β Ξ± i π π (Ξ» x β Ξ² x i)

```

In the proof above, we assume the following typing judgments:

`````` Ξ± : β i β π i β Subuniverses π¨
π : β£ π β£
π : β₯ π β₯ π β β£ π¨ β£
Ξ² : Im π β β I π
``````

and we must prove `(π Μ π¨) π β β I π`. In this case, Agda will fill in the proof term `Ξ» i β Ξ± i π π (Ξ» x β Ξ² x i)` automatically with the command `C-c C-a`.

Next, subuniverses are closed under the action of term operations.

```
module _ {π€ π¦ : Universe} where

sub-term-closed : {π§ : Universe}{X : π§ Μ}(π¨ : Algebra π€ π){B : Pred β£ π¨ β£ π¦}
β                (B β Subuniverses π¨) β (t : Term X)(b : X β β£ π¨ β£)
β                Ξ  x κ X , (b x β B)  β  (t Μ π¨) b β B

sub-term-closed π¨ AB (β x) b Bb = Bb x
sub-term-closed π¨ {B} Ξ± (node π π‘) b Ξ² = Ξ± π (Ξ» z β (π‘ z Μ π¨) b) (Ξ» x β sub-term-closed π¨ {B} Ξ± (π‘ x) b Ξ²)

```

In the induction step of the foregoing proof, the typing judgments of the premise are the following:

``````π¨   : Algebra π€ π
B   : Pred β£ π¨ β£ π¦
Ξ±   : B β Subuniverses π¨
π   : β£ π β£
π‘   : β₯ π β₯ π β Term X
b   : X β β£ π¨ β£
Ξ²   : β x β b x β B
``````

and the given proof term establishes the goal `(node π π‘ Μ π¨) b β B`.

Alternatively, we could express the preceeding fact using an inductive type representing images of terms.

```
data TermImage (π¨ : Algebra π€ π)(Y : Pred β£ π¨ β£ π¦) : Pred β£ π¨ β£ (π β π₯ β π€ β π¦)
where
var : β {y : β£ π¨ β£} β y β Y β y β TermImage π¨ Y
app : β π π‘ β  Ξ  x κ β₯ π β₯ π , π‘ x β TermImage π¨ Y  β (π Μ π¨) π‘ β TermImage π¨ Y

```

By what we proved above, it should come as no surprise that `TermImage π¨ Y` is a subuniverse of π¨ that contains Y.

```
TermImageIsSub : {π¨ : Algebra π€ π}{Y : Pred β£ π¨ β£ π¦} β TermImage π¨ Y β Subuniverses π¨
TermImageIsSub = app

Y-onlyif-TermImageY : {π¨ : Algebra π€ π}{Y : Pred β£ π¨ β£ π¦} β Y β TermImage π¨ Y
Y-onlyif-TermImageY {a} Ya = var Ya

```

Since `Sg π¨ Y` is the smallest subuniverse containing Y, we obtain the following inclusion.

```
SgY-onlyif-TermImageY : (π¨ : Algebra π€ π)(Y : Pred β£ π¨ β£ π¦) β Sg π¨ Y β TermImage π¨ Y
SgY-onlyif-TermImageY π¨ Y = sgIsSmallest π¨ (TermImage π¨ Y) TermImageIsSub Y-onlyif-TermImageY

```

#### Homomorphic images are subuniverses

Now that we have developed the machinery of subuniverse generation, we can prove two basic facts that play an important role in many theorems about algebraic structures. First, the image of a homomorphism is a subuniverse of its codomain.

```
hom-image-is-sub : dfunext π₯ π¦ β {π¨ : Algebra π€ π}{π© : Algebra π¦ π}

hom-image-is-sub fe {π¨}{π©} Ο π b Imfb = eq ((π Μ π©) b) ((π Μ π¨) ar) Ξ³
where
ar : β₯ π β₯ π β β£ π¨ β£
ar = Ξ» x β Inv β£ Ο β£ (Imfb x)

ΞΆ : β£ Ο β£ β ar β‘ b
ΞΆ = fe (Ξ» x β InvIsInv β£ Ο β£ (Imfb x))

Ξ³ : (π Μ π©) b β‘ β£ Ο β£ ((π Μ π¨) ar)
(π Μ π©) (β£ Ο β£ β ar) β‘β¨(β₯ Ο β₯ π ar)β»ΒΉ β©
β£ Ο β£ ((π Μ π¨) ar)   β

```

Next we prove the important fact that homomorphisms are uniquely determined by their values on a generating set.

```
hom-unique : funext π₯ π¦ β {π¨ : Algebra π€ π}{π© : Algebra π¦ π}
(X : Pred β£ π¨ β£ π€)  (g h : hom π¨ π©)
β           Ξ  x κ β£ π¨ β£ , (x β X β β£ g β£ x β‘ β£ h β£ x)
-------------------------------------------------
β           Ξ  a κ β£ π¨ β£ , (a β Sg π¨ X β β£ g β£ a β‘ β£ h β£ a)

hom-unique _ _ _ _ Ξ± a (var x) = Ξ± a x

hom-unique fe {π¨}{π©} X g h Ξ± fa (app π π Ξ²) = β£ g β£ ((π Μ π¨) π)   β‘β¨ β₯ g β₯ π π β©
(π Μ π©)(β£ h β£ β π)  β‘β¨ ( β₯ h β₯ π π )β»ΒΉ β©
β£ h β£ ((π Μ π¨) π )  β
where IH = Ξ» x β hom-unique fe {π¨}{π©} X g h Ξ± (π x) (Ξ² x)

```

In the induction step, we have the following typing judgments in the premise:

``````fe  : funext π₯ π¦
π¨   : Algebra π€ π
and, under these assumptions, we prove `β£ g β£ ((π Μ π¨) π) β‘ β£ h β£ ((π Μ π¨) π)`.