↑ Top

Basic definitions

This is the Setoid.Algebras.Basic module of the Agda Universal Algebra Library.


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

open import Overture using (π“ž ; π“₯ ; Signature )

module Setoid.Algebras.Basic {𝑆 : Signature π“ž π“₯} where

-- Imports from the Agda and the Agda Standard Library --------------------
open import Agda.Primitive   using ( _βŠ”_ ; lsuc ) renaming ( Set to Type )
open import Data.Product     using ( _,_ ; _Γ—_ ; Ξ£-syntax )
open import Function         using ( _∘_ ; Func )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid ; IsEquivalence )

open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------
open import Overture    using ( βˆ₯_βˆ₯ ; ∣_∣ )

private variable α ρ ι : Level

ov : Level β†’ Level
ov Ξ± = π“ž βŠ” π“₯ βŠ” lsuc Ξ±

Setoid Algebras

Here we define algebras over a setoid, instead of a mere type with no equivalence on it.

(This approach is inspired by the one taken, e.g., by Andreas Abel in his formalization Birkhoff’s completeness theorem; a pdf is available here.)

First we define an operator that translates an ordinary signature into a signature over a setoid domain.


open Setoid using (_β‰ˆ_ ; Carrier ) renaming  ( refl   to reflS
                                             ; sym    to symS
                                             ; trans  to transS
                                             ; isEquivalence to isEqv )

open Func renaming ( f to _⟨$⟩_ ; cong to β‰ˆcong )


EqArgs :  {𝑆 : Signature π“ž π“₯}{ΞΎ : Setoid Ξ± ρ}
 β†’        βˆ€{f g} β†’ f ≑ g β†’ (βˆ₯ 𝑆 βˆ₯ f β†’ Carrier ΞΎ) β†’ (βˆ₯ 𝑆 βˆ₯ g β†’ Carrier ΞΎ) β†’ Type _

EqArgs {ΞΎ = ΞΎ} refl u v = βˆ€ i β†’ (_β‰ˆ_ ΞΎ) (u i) (v i)


⟨_⟩ : Signature π“ž π“₯ β†’ Setoid Ξ± ρ β†’ Setoid _ _
Carrier (⟨ 𝑆 ⟩ ΞΎ) = Ξ£[ f ∈ ∣ 𝑆 ∣ ] ((βˆ₯ 𝑆 βˆ₯ f) β†’ ΞΎ .Carrier)
_β‰ˆ_ (⟨ 𝑆 ⟩ ΞΎ) (f , u) (g , v) = Ξ£[ eqv ∈ f ≑ g ] EqArgs{ΞΎ = ΞΎ} eqv u v

IsEquivalence.refl   (isEqv (⟨ 𝑆 ⟩ ΞΎ))                      = refl , Ξ» _ β†’ reflS   ΞΎ
IsEquivalence.sym    (isEqv (⟨ 𝑆 ⟩ ΞΎ))(refl , g)            = refl , Ξ» i β†’ symS    ΞΎ (g i)
IsEquivalence.trans  (isEqv (⟨ 𝑆 ⟩ ΞΎ))(refl , g)(refl , h)  = refl , Ξ» i β†’ transS  ΞΎ (g i) (h i)

A setoid algebra is just like an algebra but we require that all basic operations of the algebra respect the underlying setoid equality. The Func record packs a function (f, aka apply, aka _⟨$⟩_) with a proof (cong) that the function respects equality.


record Algebra Ξ± ρ : Type (π“ž βŠ” π“₯ βŠ” lsuc (Ξ± βŠ” ρ)) where
 field
  Domain : Setoid α ρ
  Interp : Func (⟨ 𝑆 ⟩ Domain) Domain
   --      ^^^^^^^^^^^^^^^^^^^^^^^ is a record type with two fields:
   --       1. a function  f : Carrier (⟨ 𝑆 ⟩ Domain)  β†’ Carrier Domain
   --       2. a proof cong : f Preserves _β‰ˆβ‚_ ⟢ _β‰ˆβ‚‚_ (that f preserves the setoid equalities)
 -- Actually, we already have the following: (it's called "reflexive"; see Structures.IsEquivalence)
 β‰‘β†’β‰ˆ : βˆ€{x}{y} β†’ x ≑ y β†’ (_β‰ˆ_ Domain) x y
 β‰‘β†’β‰ˆ refl = Setoid.refl Domain

open Algebra

The next three definitions are merely syntactic sugar, but they can be very useful for improving readability of our code.


𝔻[_] : Algebra Ξ± ρ β†’  Setoid Ξ± ρ
𝔻[ 𝑨 ] = Domain 𝑨

-- forgetful functor: returns the carrier of (the domain of) 𝑨, forgetting its structure
π•Œ[_] : Algebra Ξ± ρ β†’  Type Ξ±
π•Œ[ 𝑨 ] = Carrier 𝔻[ 𝑨 ]

-- interpretation of an operation symbol in an algebra
_Μ‚_ : (f : ∣ 𝑆 ∣)(𝑨 : Algebra Ξ± ρ) β†’ (βˆ₯ 𝑆 βˆ₯ f  β†’  π•Œ[ 𝑨 ]) β†’ π•Œ[ 𝑨 ]

f Μ‚ 𝑨 = Ξ» a β†’ (Interp 𝑨) ⟨$⟩ (f , a)

Sometimes we want to extract the universe level of a given algebra or its carrier. The following functions provide that information.


-- The universe level of an algebra
Level-of-Alg : {Ξ± ρ π“ž π“₯ : Level}{𝑆 : Signature π“ž π“₯} β†’ Algebra Ξ± ρ β†’ Level
Level-of-Alg {Ξ± = Ξ±}{ρ}{π“ž}{π“₯} _ = π“ž βŠ” π“₯ βŠ” lsuc (Ξ± βŠ” ρ)

-- The universe level of the carrier of an algebra
Level-of-Carrier : {Ξ± ρ π“ž π“₯  : Level}{𝑆 : Signature π“ž π“₯} β†’ Algebra Ξ± ρ β†’ Level
Level-of-Carrier {Ξ± = Ξ±} _ = Ξ±

Level lifting setoid algebra types


module _ (𝑨 : Algebra Ξ± ρ) where

 open Algebra 𝑨  using ( Interp )      renaming ( Domain to A )
 open Setoid A   using (sym ; trans )  renaming ( Carrier to ∣A∣ ; _β‰ˆ_ to _β‰ˆβ‚_ ; refl to refl₁ )

 open Level


 Lift-AlgΛ‘ : (β„“ : Level) β†’ Algebra (Ξ± βŠ” β„“) ρ

 Domain (Lift-AlgΛ‘ β„“) = record  { Carrier = Lift β„“ ∣A∣
                                ; _β‰ˆ_ = Ξ» x y β†’ lower x β‰ˆβ‚ lower y
                                ; isEquivalence = record  { refl = refl₁
                                                          ; sym = sym
                                                          ; trans = trans
                                                          }
                                }

 Interp (Lift-AlgΛ‘ β„“) ⟨$⟩ (f , la) = lift ((f Μ‚ 𝑨) (lower ∘ la))
 β‰ˆcong (Interp (Lift-AlgΛ‘ β„“)) (refl , la=lb) = β‰ˆcong (Interp 𝑨) ((refl , la=lb))

 Lift-AlgΚ³ : (β„“ : Level) β†’ Algebra Ξ± (ρ βŠ” β„“)
 Domain (Lift-AlgΚ³ β„“) =
  record  { Carrier = ∣A∣
          ; _β‰ˆ_ = Ξ» x y β†’ Lift β„“ (x β‰ˆβ‚ y)
          ; isEquivalence = record  { refl = lift refl₁
                                    ; sym = Ξ» x β†’ lift (sym (lower x))
                                    ; trans = Ξ» x y β†’ lift (trans (lower x) (lower y))
                                    }
          }

 Interp (Lift-AlgΚ³ β„“ ) ⟨$⟩ (f , la) = (f Μ‚ 𝑨) la
 β‰ˆcong (Interp (Lift-AlgΚ³ β„“)) (refl , la≑lb) = lift (β‰ˆcong (Interp 𝑨) (≑.refl , Ξ» i β†’ lower (la≑lb i)))

Lift-Alg : (𝑨 : Algebra Ξ± ρ)(β„“β‚€ ℓ₁ : Level) β†’ Algebra (Ξ± βŠ” β„“β‚€) (ρ βŠ” ℓ₁)
Lift-Alg 𝑨 β„“β‚€ ℓ₁ = Lift-AlgΚ³ (Lift-AlgΛ‘ 𝑨 β„“β‚€) ℓ₁

↑ Setoid.Algebras Setoid.Algebras.Products β†’