↑ Top

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 ( 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  : βˆ₯ 𝑆 βˆ₯ 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 ( to to _⟨$⟩_ )
  open SetoidReasoning B

  private
   g = _⟨$⟩_ ∣ gh ∣
   h = _⟨$⟩_ ∣ 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 βˆ₯ gh βˆ₯ ⟩
           (f Μ‚ 𝑩)(g ∘ a ) β‰ˆΛ˜βŸ¨ cong Interp (refl , IH) ⟩
           (f Μ‚ 𝑩)(h ∘ a)  β‰ˆΛ˜βŸ¨ compatible βˆ₯ hh βˆ₯ ⟩
           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 β„“
hh   : hom 𝑨 𝑩
gh   : hom 𝑨 𝑩

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

↑ Setoid.Subalgebras Setoid.Subalgebras.Subalgebras β†’