↑ 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 ( to 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 Ξ± ρ)(β„“ : Level) where
 open Algebra 𝑨  using ()     renaming ( Domain to A )
 open Setoid A   using (sym ; trans )  renaming ( Carrier to ∣A∣ ; _β‰ˆ_ to _β‰ˆβ‚_ ; refl to refl₁ )
 open Level


 Lift-AlgΛ‘ : Algebra (Ξ± βŠ” β„“) ρ
 Lift-AlgΛ‘ .Domain                        = record  { Carrier = Lift β„“ ∣A∣
                                                    ; _β‰ˆ_ = Ξ» x y β†’ lower x β‰ˆβ‚ lower y
                                                    ; isEquivalence = record
                                                      { refl = refl₁
                                                      ; sym = sym
                                                      ; trans = trans
                                                      }
                                                    }
 Lift-AlgΛ‘ .Interp ⟨$⟩ (f , la)           = lift $ (f Μ‚ 𝑨) (lower ∘ la)
 Lift-AlgΛ‘ .Interp .β‰ˆcong (refl , la=lb)  = β‰ˆcong (Interp 𝑨) (refl , la=lb)


 Lift-AlgΚ³ : Algebra Ξ± (ρ βŠ” β„“)
 Lift-Algʳ .Domain                        = record  { Carrier = ∣A∣
                                                    ; _β‰ˆ_ = (Lift β„“) βˆ˜β‚‚ _β‰ˆβ‚_
                                                    ; isEquivalence = record
                                                      { refl = lift refl₁
                                                      ; sym = lift ∘ sym ∘ lower
                                                      ; trans = Ξ» x y β†’ lift $ trans (lower x) (lower y)
                                                      }
                                                    }
 Lift-AlgΚ³ .Interp ⟨$⟩ (f , la)           = (f Μ‚ 𝑨) la
 Lift-AlgΚ³ .Interp .β‰ˆcong (refl , la≑lb)  = lift $ β‰ˆcong (Interp 𝑨) (≑.refl , (lower ∘ la≑lb))


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

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