---
layout: default
title : "Setoid.Subalgebras.Subuniverses module (The Agda Universal Algebra Library)"
date : "2021-07-11"
author: "agda-algebras development team"
---

#### Subuniverses of setoid algebras

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


<!--
```agda
{-# OPTIONS --cubical-compatible --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 ( proj₁ ; projβ‚‚ ; ArityOf ; Im_βŠ†_ )
open import Overture.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 `π•Œ[ 𝑨 ]`.


```agda
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 : OperationSymbolsOf 𝑆` and
`a : ArityOf 𝑆 𝑓 β†’ π•Œ[ 𝑨 ]`.)

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.


```agda
  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`.


```agda
  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.


```agda
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  : ArityOf 𝑆 f β†’ Setoid.Subalgebras.A 𝑨
    f  : OperationSymbolsOf 𝑆
    Οƒ  : (i : I) β†’ π’œ i ∈ Subuniverses 𝑨

and we must prove `(f ^ 𝑨) a ∈ β‹‚ I π’œ`.  (The command `C-c C-a` works in this case;
Agda fills in the proof term `Ξ» i β†’ Οƒ i f a (Ξ» x β†’ Ξ½ x i)` automatically.)


```agda
module _ {𝑨 : Algebra Ξ± ρᡃ} where
  private A = π•Œ[ 𝑨 ]
  open Setoid using ( Carrier )
  open Environment 𝑨
  open Func renaming ( to 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  : ArityOf 𝑆 f β†’ Term X
    f  : OperationSymbolsOf 𝑆
    Οƒ  : 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.


```agda
  data TermImage (B : Pred A ρᡃ) : Pred A (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρᡃ) where
    var : βˆ€ {b : A} β†’ b ∈ B β†’ b ∈ TermImage B
    app : βˆ€ f ts β†’  ((i : ArityOf 𝑆 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`.


```agda
  module _ {𝑩 : Algebra Ξ² ρᡇ} (gh hh : hom 𝑨 𝑩) where
    open Algebra 𝑩  using ( Interp )  renaming ( Domain to B )
    open Setoid B   using ( _β‰ˆ_ ; sym )
    open Func       using ( cong )    renaming ( to to _⟨$⟩_ )
    open SetoidReasoning B

    private
      g = _⟨$⟩_ (proj₁ gh)
      h = _⟨$⟩_ (proj₁ hh)

    open IsHom
    open Environment 𝑩

    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 (projβ‚‚ gh) ⟩
              (f ^ 𝑩)(g ∘ a )  β‰ˆΛ˜βŸ¨ cong Interp (refl , IH) ⟩
              (f ^ 𝑩)(h ∘ a)   β‰ˆΛ˜βŸ¨ compatible (projβ‚‚ hh) ⟩
              h ((f ^ 𝑨) a )   ∎
```


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

    SgGa : Im a βŠ† Sg 𝑨 G
    a    : ArityOf 𝑆 f β†’ Subuniverses 𝑨
    f    : OperationSymbolsOf 𝑆
    Οƒ    : (x : A) β†’ x ∈ G β†’ g x β‰ˆ h x
    G    : Pred A β„“
    hh   : hom 𝑨 𝑩
    gh   : hom 𝑨 𝑩

and, under these assumptions, we proved `g ((f ^ 𝑨) a) β‰ˆ h ((f ^ 𝑨) a)`.