 ### Subuniverses

This is the Base.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 Overture using ( 𝓞 ; 𝓥 ; Signature )

module Base.Subalgebras.Subuniverses {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Agda.Primitive       using () renaming ( Set to Type )
open import Function             using ( _∘_ )
open import Level                using ( Level ; _⊔_ )
open import Relation.Unary       using ( Pred ; _∈_ ; _⊆_ ; ⋂ )
open import Axiom.Extensionality.Propositional
using () renaming ( Extensionality to funext )
open import Relation.Binary.PropositionalEquality
using ( module ≡-Reasoning ; _≡_ )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Overture                     using ( ∣_∣ ; ∥_∥ ; _⁻¹ )
open import Base.Relations               using ( Im_⊆_ )
open import Base.Equality                using ( swelldef )
open import Base.Algebras       {𝑆 = 𝑆}  using ( Algebra ; _̂_ ; ov )
open import Base.Homomorphisms  {𝑆 = 𝑆}  using ( hom )
open import Base.Terms          {𝑆 = 𝑆}  using ( Term ; ℊ ; node ; _⟦_⟧ )

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 ∣ 𝑨 ∣ β
sSub : 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)`.