Agda UALib ↑

Algebras

This section presents the Algebras.Algebras module of the Agda Universal Algebra Library.


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

module Algebras.Algebras where

open import Algebras.Signatures public

Algebra types

Recall, the type Signature π“ž π“₯ was defined in the Algebras.Signatures module as the dependent pair type Ξ£ F κž‰ π“ž Μ‡ , (F β†’ π“₯ Μ‡), and the type \af{Op} of operation symbols was defined in Relations.Discrete as the function type Op I A = (I β†’ A) β†’ A.

For a fixed signature 𝑆 : Signature π“ž π“₯ and universe 𝓀, we define the type of algebras in the signature 𝑆 (or 𝑆-algebras) and with domain (or carrier) of type 𝓀 Μ‡ as follows.1


Algebra : (𝓀 : Universe)(𝑆 : Signature π“ž π“₯) β†’ π“ž βŠ” π“₯ βŠ” 𝓀 ⁺ Μ‡

Algebra 𝓀 𝑆 = Ξ£ A κž‰ 𝓀 Μ‡ ,                     -- the domain
              Ξ  f κž‰ ∣ 𝑆 ∣ , Op (βˆ₯ 𝑆 βˆ₯ f) A    -- the basic operations

We might refer to inhabitants of this type as ∞-algebras because their domains can be of arbitrary type and need not be truncated at some level and, in particular, need to be a set. (See the Relations.Truncation module.)

We might take this opportunity to define the type of 0-algebras, that is, algebras whose domains are sets, which is probably closer to what most of us think of when doing informal universal algebra. However, below we will only need to know that the domains of certain algebras are sets in a few places in the UALib, so it seems preferable to work with general (∞-)algebras throughout and then explicitly postulate uniquness of identity proofs when and only when necessary.

Algebras as record types

Some people prefer to represent algebraic structures in type theory using records, and for those folks we offer the following (equivalent) definition.


record algebra (𝓀 : Universe) (𝑆 : Signature π“ž π“₯) : (π“ž βŠ” π“₯ βŠ” 𝓀) ⁺ Μ‡ where
 constructor mkalg
 field
  univ : 𝓀 Μ‡
  op : (f : ∣ 𝑆 ∣) β†’ ((βˆ₯ 𝑆 βˆ₯ f) β†’ univ) β†’ univ

This representation of algebras as inhabitants of a record type is equivalent to the representation using Sigma types in the sense that a bi-implication between the two representations is obvious.


module _ {𝑆 : Signature π“ž π“₯} where

 open algebra

 algebraβ†’Algebra : algebra 𝓀 𝑆 β†’ Algebra 𝓀 𝑆
 algebraβ†’Algebra 𝑨 = (univ 𝑨 , op 𝑨)

 Algebraβ†’algebra : Algebra 𝓀 𝑆 β†’ algebra 𝓀 𝑆
 Algebraβ†’algebra 𝑨 = mkalg ∣ 𝑨 ∣ βˆ₯ 𝑨 βˆ₯

Operation interpretation syntax

We now define a convenient shorthand for the interpretation of an operation symbol. This looks more similar to the standard notation one finds in the literature as compared to the double bar notation we started with, so we will use this new notation almost exclusively in the remaining modules of the UALib.


 _Μ‚_ : (𝑓 : ∣ 𝑆 ∣)(𝑨 : Algebra 𝓀 𝑆) β†’ (βˆ₯ 𝑆 βˆ₯ 𝑓  β†’  ∣ 𝑨 ∣) β†’ ∣ 𝑨 ∣

 𝑓 Μ‚ 𝑨 = Ξ» π‘Ž β†’ (βˆ₯ 𝑨 βˆ₯ 𝑓) π‘Ž

So, if 𝑓 : ∣ 𝑆 ∣ is an operation symbol in the signature 𝑆, and if π‘Ž : βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣ is a tuple of the appropriate arity, then (𝑓 Μ‚ 𝑨) π‘Ž denotes the operation 𝑓 interpreted in 𝑨 and evaluated at π‘Ž.

Level lifting algebra types

Recall, in the section on level lifting and lowering, we described the difficulties one may encounter when working with a noncumulative universe hierarchy. We made a promise to provide some domain-specific level lifting and level lowering methods. Here we fulfill this promise by supplying a couple of bespoke tools designed specifically for our operation and algebra types.



module _ {π“˜ : Universe} {I : π“˜ Μ‡}{A : 𝓀 Μ‡} where

 open Lift

 Lift-op : Op I A β†’ (𝓦 : Universe) β†’ Op I (Lift{𝓦} A)
 Lift-op f 𝓦 = Ξ» x β†’ lift (f (Ξ» i β†’ lower (x i)))

module _ {𝑆 : Signature π“ž π“₯}  where

 Lift-alg : Algebra 𝓀 𝑆 β†’ (𝓦 : Universe) β†’ Algebra (𝓀 βŠ” 𝓦) 𝑆
 Lift-alg 𝑨 𝓦 = Lift ∣ 𝑨 ∣ , (Ξ» (𝑓 : ∣ 𝑆 ∣) β†’ Lift-op (𝑓 Μ‚ 𝑨) 𝓦)

 open algebra

 Lift-alg-record-type : algebra 𝓀 𝑆 β†’ (𝓦 : Universe) β†’ algebra (𝓀 βŠ” 𝓦) 𝑆
 Lift-alg-record-type 𝑨 𝓦 = mkalg (Lift (univ 𝑨)) (Ξ» (f : ∣ 𝑆 ∣) β†’ Lift-op ((op 𝑨) f) 𝓦)

What makes the Lift-alg type so useful for resolving type level errors involving algebras is the nice properties it possesses. Indeed, the UALib contains formal proofs of the following facts.

Compatibility of binary relations

We now define the function compatible so that, if 𝑨 is an algebra and R a binary relation, then compatible 𝑨 R will represents the assertion that R is compatible with all basic operations of 𝑨. <!– Recall (from Relations.Discrete) that informally this means for every operation symbol 𝑓 : ∣ 𝑆 ∣ and all pairs u v : βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣ of tuples from the domain of 𝑨, the following implication holds:

Β Β  (Ξ  i κž‰ I , R (u i) (u i)) Β Β  β†’ Β Β  R ((𝑓 Μ‚ 𝑨) u) ((𝑓 Μ‚ 𝑨) v).

In other terms, βˆ€ 𝑓 β†’ (𝑓 Μ‚ 𝑨) |: R. –> The formal definition is immediate since all the work is done by the relation |: (which we already defined in Relations.Discrete).


 compatible : (𝑨 : Algebra 𝓀 𝑆) β†’ Rel ∣ 𝑨 ∣ 𝓦 β†’ π“ž βŠ” 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
 compatible  𝑨 R = βˆ€ 𝑓 β†’ (𝑓 Μ‚ 𝑨) |: R

Recall, the |: type was defined in Relations.Discrete module.

Compatibility of continuous relationsβ˜…

In the Relations.Continuous module, we defined a function called cont-compatible-op to represent the assertion that a given continuous relation is compatible with a given operation. With that, it is easy to define a function, which we call cont-compatible, representing compatibility of a continuous relation with all operations of an algebra. Similarly, we define the analogous dep-compatible function for the (even more general) type of dependent relations.


module _ {𝓀 𝓦 : Universe} {I : π“₯ Μ‡} {𝑆 : Signature π“ž π“₯} where
 open import Relations.Continuous using (ContRel; DepRel; cont-compatible-op; dep-compatible-op)

 cont-compatible : (𝑨 : Algebra 𝓀 𝑆) β†’ ContRel I ∣ 𝑨 ∣ 𝓦 β†’ π“ž βŠ” 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
 cont-compatible 𝑨 R = Ξ  𝑓 κž‰ ∣ 𝑆 ∣ , cont-compatible-op (𝑓 Μ‚ 𝑨) R

 dep-compatible : (π’œ : I β†’ Algebra 𝓀 𝑆) β†’ DepRel I (Ξ» i β†’ ∣ π’œ  i ∣) 𝓦 β†’ π“ž βŠ” 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
 dep-compatible π’œ R = Ξ  𝑓 κž‰ ∣ 𝑆 ∣ , dep-compatible-op (Ξ» i β†’ 𝑓 Μ‚ (π’œ i)) R

β˜… Sections marked with an asterisk include new types that are more abstract and general (and frankly more interesting) than the ones presented in other sections. Consequently, such sections expect a higher degree of sophistication and/or effort from the reader/user. Moreover, the types defined in starred sections are used in only a few other places in the Agda UALib, so they may be safely skimmed over or skipped.

[1] In classical universal algebra, the domain of an algebra 𝑨 is usualled called the β€œuniverse” of 𝑨. We avoid this terminology and reserve universe for use in defining the type hierarchy. (See the Agda Universes</a> section of the Overture.Preliminaries module.



← Algebras.Signatures Algebras.Products β†’