Skip to content

Setoid.Subalgebras.Subuniverses

Subuniverses of setoid algebras

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

A subuniverse of 𝑨 is a subset of its carrier that is closed under the basic operations: whenever every entry of an argument tuple lies in the subset, so does the result of applying an operation to that tuple. Subuniverses are the concrete counterpart of the abstract _≀_ of Setoid.Subalgebras.Basic, which asks only for an embedding and says nothing about carriers being subsets.

This module defines Subuniverses, the predicate itself, and the subuniverse Sg generated by an arbitrary subset, given inductively by a generator constructor and an operation constructor. The two facts that make generation usable are sgIsSub, that Sg G really is a subuniverse, and sgIsSmallest, that it is contained in every subuniverse containing G. Also here: closure of subuniverses under arbitrary intersection (β‹‚s), which is what makes the lattice of Setoid.Subalgebras.CompleteLattice complete; and hom-unique, that two homomorphisms agreeing on a generating set agree everywhere.

The term-level results are the remainder. sub-term-closed says a subuniverse is closed under the term operations: if every variable is sent into B, so is the value of any term. TermImage approaches the same ground from the other side, as the inductively defined set of values of terms with arguments drawn from B, and TermImageIsSub shows it is a subuniverse containing B (B-onlyif-TermImageB).

Those two facts pin TermImage B down completely: it is the subuniverse generated by B. SgB-onlyif-TermImageB gives one inclusion, since Sg B is the smallest subuniverse containing B, and TermImageB-onlyif-SgB gives the other by induction on TermImage, a generator already lying in Sg B and Sg B being closed under the operations. So the generated subuniverse admits two equivalent descriptions, top-down as the least subuniverse above B and bottom-up as the set of values of terms over B, and a proof may use whichever is convenient.

One converse is genuinely absent, and it is not this one: sub-term-closed is not accompanied by a proof that closure under the term operations implies membership in Subuniverses.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Subalgebras.Subuniverses 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_βŠ†_
                                                 ; OperationSymbolsOf ; π“ž ; π“₯ ; Signature ; 𝑆 )
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 π•Œ[ 𝑨 ].

module _ {𝑆 : Signature π“ž π“₯}(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ) where
  private A = π•Œ[ 𝑨 ] -- the forgetful functor

  Subuniverses : Pred (Pred A β„“) (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” β„“ )
  Subuniverses B =
    (f : OperationSymbolsOf 𝑆) (a : ArityOf 𝑆 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.

  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  : 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.)

module _ {𝑆 : Signature π“ž π“₯}{𝑨 : 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.

  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

  -- The reverse inclusion, by induction on TermImage: a generator is already in
  -- `Sg B`, and `Sg B` is closed under the operations.
  TermImageB-onlyif-SgB : (B : Pred A ρᡃ) β†’ TermImage B βŠ† Sg 𝑨 B
  TermImageB-onlyif-SgB B (var Ba) = var Ba
  TermImageB-onlyif-SgB B (app f ts Ξ½) = app f ts (Ξ» i β†’ TermImageB-onlyif-SgB B (Ξ½ i))

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 ( 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).