#### Subuniverses of setoid algebras

This is the Setoid.Subalgebras.Subuniverses module of the Agda Universal Algebra Library.

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

open import Overture using (π ; π₯ ; Signature)

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

-- Imports from Agda and the Agda Standard Library ----------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ )
open import Function         using ( _β_ ; Func )
open import Level            using (Level ;  _β_ )
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( Pred ; _β_ ; _β_ ; β )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebra Library ----------------------------------
open import Overture        using ( β£_β£ ; β₯_β₯ )
open import Base.Relations  using ( Im_β_ )

open import Base.Terms            {π = π} using ( Term ; β ; node )
open import Setoid.Algebras       {π = π} using ( Algebra ; π[_] ; _Μ_ ; ov )
open import Setoid.Terms          {π = π} using ( module Environment )
open import Setoid.Homomorphisms  {π = π} using ( hom ; IsHom )

private variable
Ξ± Ξ² Ξ³ Οα΅ Οα΅ ΟαΆ β Ο : Level
X : Type Ο

```

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 _ (π¨ : Algebra Ξ± Οα΅) where
private A = π[ π¨ ] -- the forgetful functor

Subuniverses : Pred (Pred A β) (π β π₯ β Ξ± β β )
Subuniverses B = β f a β Im a β B β (f Μ π¨) a β B

-- Subuniverses as a record type
record Subuniverse : Type(ov (Ξ± β β)) where
constructor mksub
field
sset  : Pred A β
isSub : sset β Subuniverses

-- Subuniverse Generation
data Sg (G : Pred A β) : Pred A (π β π₯ β Ξ± β β) where
var : β {v} β v β G β v β Sg G
app : β f a β Im a β Sg G β (f Μ π¨) a β Sg G

```

(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 : {G : Pred A β} β Sg G β Subuniverses
sgIsSub = app

```

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

```
sgIsSmallest :  {G : Pred A Οα΅}(B : Pred A Οα΅)
β              B β Subuniverses  β  G β B  β  Sg G β B

sgIsSmallest _ _ GβB (var Gx) = GβB Gx
sgIsSmallest B Bβ€A GβB {.((f Μ π¨) a)} (app f a SgGa) = Goal
where
IH : Im a β B
IH i = sgIsSmallest B Bβ€A GβB (SgGa i)

Goal : (f Μ π¨) a β B
Goal = Bβ€A f a IH

```

When the element of `Sg G` is constructed as `app f a SgGa`, we may assume (the induction hypothesis) that the arguments in the tuple `a` belong to `B`. Then the result of applying `f` to `a` also belongs to `B` since `B` is a subuniverse.

```
module _ {π¨ : Algebra Ξ± Οα΅} where
private A = π[ π¨ ]

βs :  {ΞΉ : Level}(I : Type ΞΉ){Ο : Level}{π : I β Pred A Ο}
β    (β i β π i β Subuniverses π¨) β β I π β Subuniverses π¨

βs I Ο f a Ξ½ = Ξ» i β Ο i f a (Ξ» x β Ξ½ x i)

```

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

``````Ξ½  : Im a β β I π
a  : β₯ π β₯ f β Setoid.Subalgebras.A π¨
f  : β£ π β£
Ο  : (i : I) β π i β Subuniverses π¨
``````

and we must prove `(f Μ π¨) a β β I π`. When we did this with the old Algebra type, Agda could fill in the proof term `Ξ» i β Ο i f a (Ξ» x β Ξ½ x i)` automatically using `C-c C-a`, but this doesnβt work for Algebra as weβve implemented it. We get the error βAgsy does not support copatterns yet.β We should fix the implementation to resolve this.

```
module _ {π¨ : Algebra Ξ± Οα΅} where
private A = π[ π¨ ]
open Setoid using ( Carrier )
open Environment π¨
open Func renaming ( f to _β¨\$β©_ )

-- subuniverses are closed under the action of term operations
sub-term-closed :  (B : Pred A β)
β                 (B β Subuniverses π¨)
β                 (t : Term X)
β                 (b : Carrier (Env X))
β                 (β x β (b x β B)) β (β¦ t β§ β¨\$β© b) β B

sub-term-closed _ _ (β x) b Bb = Bb x
sub-term-closed B Bβ€A (node f t)b Ξ½ =
Bβ€A f  (Ξ» z β β¦ t z β§ β¨\$β© b) Ξ» x β sub-term-closed B Bβ€A (t x) b Ξ½

```

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

``````Ξ½  : (x : X) β b x β B
b  : Setoid.Carrier (Env X)
t  : β₯ π β₯ f β Term X
f  : β£ π β£
Ο  : B β Subuniverses π¨
B  : Pred A Ο
Ο  : Level
π¨  : Algebra Ξ± Οα΅
``````

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 (B : Pred A Οα΅) : Pred A (π β π₯ β Ξ± β Οα΅) where
var : β {b : A} β b β B β b β TermImage B
app : β f ts β  ((i : β₯ π β₯ f) β ts i β TermImage B)  β (f Μ π¨) ts β TermImage B

-- `TermImage B` is a subuniverse of π¨ that contains B.
TermImageIsSub : {B : Pred A Οα΅} β TermImage B β Subuniverses π¨
TermImageIsSub = app

B-onlyif-TermImageB : {B : Pred A Οα΅} β B β TermImage B
B-onlyif-TermImageB Ba = var Ba

-- Since `Sg B` is the smallest subuniverse containing B, we obtain the following inclusion.
SgB-onlyif-TermImageB : (B : Pred A Οα΅) β Sg π¨ B β TermImage B
SgB-onlyif-TermImageB B = sgIsSmallest π¨ (TermImage B) TermImageIsSub B-onlyif-TermImageB

```

A basic but important fact about homomorphisms is that they are uniquely determined by the values they take on a generating set. This is the content of the next theorem, which we call `hom-unique`.

```
module _ {π© : Algebra Ξ² Οα΅} (gh hh : hom π¨ π©) where
open Algebra π©  using ( Interp )  renaming (Domain to B )
open Setoid B   using ( _β_ ; sym )
open Func       using ( cong )    renaming (f to _β¨\$β©_ )
open SetoidReasoning B

private
g = _β¨\$β©_ β£ gh β£
h = _β¨\$β©_ β£ hh β£

open IsHom

hom-unique :  (G : Pred A β) β ((x : A) β (x β G β g x β h x))
β            (a : A) β (a β Sg π¨ G β g a β h a)

hom-unique G Ο a (var Ga) = Ο a Ga
hom-unique G Ο .((f Μ π¨) a) (app f a SgGa) = Goal
where
IH : β i β h (a i) β g (a i)
IH i = sym (hom-unique G Ο (a i) (SgGa i))

Goal : g ((f Μ π¨) a) β h ((f Μ π¨) a)
Goal =  begin
g ((f Μ π¨) a)   ββ¨ compatible β₯ gh β₯ β©
(f Μ π©)(g β a ) βΛβ¨ cong Interp (refl , IH) β©
h ((f Μ π¨) a )  β

```

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

``````SgGa : Im a β Sg π¨ G
a    : β₯ π β₯ f β Subuniverses π¨
f    : β£ π β£
Ο    : (x : A) β x β G β g x β h x
G    : Pred A β
and, under these assumptions, we proved `g ((f Μ π¨) a) β h ((f Μ π¨) a)`.