Skip to content

Setoid.Subalgebras.Subuniverses

Subuniverses of setoid algebras

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

{-# 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 π•Œ[ 𝑨 ].

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.

  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 _ {𝑨 : 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

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