↑ Top


Basic definitions for algebras over setoids

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

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

open import Base.Algebras.Basic 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 ( _∘_ )
open import Function.Bundles 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 Base.Overture.Preliminaries 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

It should be clear that the two types Algebroid and Algebra are equivalent. (We tend to use the latter throughout most of the agda-algebras library.)

open Algebra

-- Forgetful Functor
π•Œ[_] : Algebra Ξ± ρ β†’  Type Ξ±
π•Œ[ 𝑨 ] = Carrier (Domain 𝑨)

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

-- The universe level of a Algebra

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

Level-of-Carrier : {Ξ± ρ π“ž π“₯  : Level}{𝑆 : Signature π“ž π“₯} β†’ Algebra Ξ± ρ β†’ Level
Level-of-Carrier {Ξ± = Ξ±} _ = Ξ±


open Algebra

_Μ‚_ : (f : ∣ 𝑆 ∣)(𝑨 : Algebra Ξ± ρ) β†’ (βˆ₯ 𝑆 βˆ₯ f  β†’  π•Œ[ 𝑨 ]) β†’ π•Œ[ 𝑨 ]

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

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 β†’