Subuniverses

This is 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.Basic using ( ๐ ; ๐ฅ ; Signature )

module Subalgebras.Subuniverses {๐ : Signature ๐ ๐ฅ} where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Agda.Primitive using ( _โ_ ; lsuc ; Level ) renaming ( Set to Type )
open import Axiom.Extensionality.Propositional
using () renaming (Extensionality to funext)
open import Function.Base  using ( _โ_ )
open import Relation.Binary.PropositionalEquality
using ( module โก-Reasoning ; _โก_ )
open import Relation.Unary using ( Pred ; _โ_ ; _โ_ ; โ )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Overture.Preliminaries      using ( โฃ_โฃ ; โฅ_โฅ ; _โปยน )
open import Relations.Discrete          using ( Im_โ_ )
open import Equality.Welldefined        using ( swelldef )
open import Algebras.Basic              using ( Algebra ; _ฬ_ )
open import Algebras.Products   {๐ = ๐} using ( ov )
open import Terms.Basic         {๐ = ๐} using ( Term ; โ ; node )
open import Terms.Operations    {๐ = ๐} using ( _โฆ_โง )
open import Homomorphisms.Basic {๐ = ๐} using ( hom )

private variable ฮฑ ฮฒ ๐ง : Level

```

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 `โฃ ๐จ โฃ`.

```Subuniverses : (๐จ : Algebra ฮฑ ๐) โ Pred (Pred โฃ ๐จ โฃ ฮฒ) (๐ โ ๐ฅ โ ฮฑ โ ฮฒ)

Subuniverses ๐จ B = (๐ : โฃ ๐ โฃ)(๐ : โฅ ๐ โฅ ๐ โ โฃ ๐จ โฃ) โ Im ๐ โ B โ (๐ ฬ ๐จ) ๐ โ B

```

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 ฮฑ ๐} : Type(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 : โ f a โ Im a โ Sg ๐จ X โ (f ฬ ๐จ) a โ Sg ๐จ X

```

(The inferred types in the `app` constructor are `f : โฃ ๐ โฃ` and `a : โฅ ๐ โฅ ๐ โ โฃ ๐จ โฃ`.)

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.

```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 : {๐ก : Level}(๐จ : Algebra ฮฑ ๐){X : Pred โฃ ๐จ โฃ ฮฒ}(Y : Pred โฃ ๐จ โฃ ๐ก)
โ             Y โ Subuniverses ๐จ  โ  X โ Y  โ  Sg ๐จ X โ Y

sgIsSmallest _ _ _ XinY (var Xv) = XinY Xv
sgIsSmallest ๐จ Y YsubA XinY (app f a SgXa) = Yfa
where
IH : Im a โ Y
IH i = sgIsSmallest ๐จ Y YsubA XinY (SgXa i)

Yfa : (f ฬ ๐จ) a โ Y
Yfa = YsubA f a IH

```

When the element of `Sg X` is constructed as `app f a SgXa`, we may assume (the induction hypothesis) that the arguments in the tuple `a` belong to `Y`. Then the result of applying `f` to `a` 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.

```โs : {๐ : Level}{๐จ : Algebra ฮฑ ๐}{I : Type ๐}{๐ : I โ Pred โฃ ๐จ โฃ ฮฒ}
โ   (โ i โ ๐ i โ Subuniverses ๐จ) โ โ I ๐ โ Subuniverses ๐จ

โs ฯ f a ฮฝ = ฮป i โ ฯ i f a (ฮป x โ ฮฝ x i)

```

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

`````` ฯ : โ i โ ๐ i โ Subuniverses ๐จ
f : โฃ ๐ โฃ
a : โฅ ๐ โฅ ๐ โ โฃ ๐จ โฃ
ฮฝ : Im ๐ โ โ I ๐
``````

and we must prove `(f ฬ ๐จ) a โ โ I ๐`. In this case, Agda will fill in the proof term `ฮป i โ ฯ i f a (ฮป x โ ฮฝ x i)` automatically with the command `C-c C-a`.

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

```sub-term-closed : {๐ง : Level}{X : Type ๐ง}(๐จ : 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 f t)b ฮฝ =
ฯ f  (ฮป z โ (๐จ โฆ t z โง) b) ฮป x โ sub-term-closed ๐จ{B} ฯ (t x) b ฮฝ

```

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

``````๐จ   : Algebra ฮฑ ๐
B   : Pred โฃ ๐จ โฃ ฮฒ
ฯ   : B โ Subuniverses ๐จ
f   : โฃ ๐ โฃ
t   : โฅ ๐ โฅ ๐ โ Term X
b   : X โ โฃ ๐จ โฃ
ฮฝ   : โ x โ b x โ B
``````

and the given proof term establishes the goal `๐จ โฆ node f t โง 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

```

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

```open โก-Reasoning

hom-unique : swelldef ๐ฅ ฮฒ โ {๐จ : 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 wd {๐จ}{๐ฉ} X g h ฯ fa (app ๐ a ฮฝ) = Goal
where
IH : โ x โ โฃ g โฃ (a x) โก โฃ h โฃ (a x)
IH x = hom-unique wd{๐จ}{๐ฉ} X g h ฯ (a x) (ฮฝ x)

Goal : โฃ g โฃ ((๐ ฬ ๐จ) a) โก โฃ h โฃ ((๐ ฬ ๐จ) a)
Goal = โฃ g โฃ ((๐ ฬ ๐จ) a)   โกโจ โฅ g โฅ ๐ a โฉ
(๐ ฬ ๐ฉ)(โฃ g โฃ โ a ) โกโจ wd (๐ ฬ ๐ฉ) (โฃ g โฃ โ a) (โฃ h โฃ โ a) IH โฉ
(๐ ฬ ๐ฉ)(โฃ h โฃ โ a)  โกโจ ( โฅ h โฅ ๐ a )โปยน โฉ
โฃ h โฃ ((๐ ฬ ๐จ) a )  โ

```

In the induction step, the following typing judgments are assumed:

``````wd  : swelldef ๐ฅ ฮฒ
๐จ   : Algebra ฮฑ ๐
๐ฉ   : Algebra ฮฒ ๐
X   : Pred โฃ ๐จ โฃ ฮฑ
g h  : hom ๐จ ๐ฉ
ฯ   : ฮ  x ๊ โฃ ๐จ โฃ , (x โ X โ โฃ g โฃ x โก โฃ h โฃ x)
fa  : โฃ ๐จ โฃ
fa  = (๐ ฬ ๐จ) a
๐   : โฃ ๐ โฃ
a   : โฅ ๐ โฅ ๐ โ โฃ ๐จ โฃ
ฮฝ   : Im a โ Sg ๐จ X
``````

and, under these assumptions, we proved `โฃ g โฃ ((๐ ฬ ๐จ) a) โก โฃ h โฃ ((๐ ฬ ๐จ) a)`.