diff --git a/docs/Base.Relations.Continuous.tex b/docs/Base.Relations.Continuous.tex deleted file mode 100644 index 242ce3e..0000000 --- a/docs/Base.Relations.Continuous.tex +++ /dev/null @@ -1,187 +0,0 @@ ---- -layout: default -title : "Base.Relations.Continuous module (The Agda Universal Algebra Library)" -date : "2021-02-28" -author: "[agda-algebras development team][]" ---- - -### Continuous Relations - -This is the [Base.Relations.Continuous][] module of the [Agda Universal Algebra Library][]. - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-module Base.Relations.Continuous where
-
--- Imports from Agda and the Agda Standard Library -------------------------------
-open import Agda.Primitive  using () renaming ( Set to Type )
-open import Level           using ( _⊔_ ; suc ; Level  )
-
--- Imports from agda-algebras ----------------------------------------------------
-open import Overture        using ( Π ; Π-syntax ; Op ; arity[_] )
-
-private variable α ρ : Level
-
-
- -#### Motivation - -In set theory, an n-ary relation on a set `A` is simply a subset of the n-fold product `A × A × ⋯ × A`. As such, we could model these as predicates over the type `A × A × ⋯ × A`, or as relations of type `A → A → ⋯ → A → Type β` (for some universe β). - -To implement such a relation in type theory, we would need to know the arity in advance, and then somehow form an n-fold arrow →. - -It's easier and more general to instead define an arity type `I : Type 𝓥`, and define the type representing `I`-ary relations on `A` as the function type `(I → A) → Type β`. - -Then, if we are specifically interested in an n-ary relation for some natural number `n`, we could take `I` to be a finite set (e.g., of type `Fin n`). - -Below we define `Rel` to be the type `(I → A) → Type β` and we call this the type of *continuous relations*. This generalizes "discrete" relations (i.e., relations of finite arity---unary, binary, etc), defined in the standard library since inhabitants of the continuous relation type can have arbitrary arity. - -The relations of type `Rel` not completely general, however, since they are defined over a single type. Said another way, they are *single-sorted* relations. We will remove this limitation when we define the type of *dependent continuous relations* later in the module. - -Just as `Rel A β` is the single-sorted special case of the multisorted `REL A B β` in the standard library, so too is our continuous version, `Rel I A β`, the single-sorted special case of a completely general type of relations. - -The latter represents relations that not only have arbitrary arities, but also are defined over arbitrary families of types. - -Concretely, given an arbitrary family `A : I → Type α` of types, we may have a relation from `A i` to `A j` to `A k` to …, where the collection represented by the "indexing" type `I` might not even be enumerable. - -We refer to such relations as *dependent continuous relations* (or *dependent relations* for short) because the definition of a type that represents them requires depedent types. - -The `REL` type that we define [below](Base.Relations.Continuous.html#dependent-relations) manifests this completely general notion of relation. - -**Warning**! The type of binary relations in the standard library's `Relation.Binary` module is also called `Rel`. Therefore, to use both the discrete binary relation from the standard library, and our continuous relation type, we recommend renaming the former when importing with a line like this - -`open import Relation.Binary renaming ( REL to BinREL ; Rel to BinRel )` - - -#### Continuous and dependent relations - -Here we define the types `Rel` and `REL`. The first of these represents predicates of arbitrary arity over a single type `A`. As noted above, we call these *continuous relations*. - -The definition of `REL` goes even further and exploits the full power of dependent types resulting in a completely general relation type, which we call the type of *dependent relations*. - -Here, the tuples of a relation of type `REL I 𝒜 β` inhabit the dependent function type `𝒜 : I → Type α` (where the codomain may depend on the input coordinate `i : I` of the domain). - -Heuristically, we can think of an inhabitant of type `REL I 𝒜 β` as a relation from `𝒜 i` to `𝒜 j` to `𝒜 k` to …. - -(This is only a rough heuristic since `I` could denote an uncountable collection.) See the discussion below for a more detailed explanation. - -
-
-module _ {𝓥 : Level} where
- ar : Type (suc 𝓥)
- ar = Type 𝓥
-
--- Relations of arbitrary arity over a single sort.
- Rel : Type α → ar → {ρ : Level} → Type (α ⊔ 𝓥 ⊔ suc ρ)
- Rel A I {ρ} = (I → A) → Type ρ
-
- Rel-syntax : Type α → ar → (ρ : Level) → Type (𝓥 ⊔ α ⊔ suc ρ)
- Rel-syntax A I ρ = Rel A I {ρ}
-
- syntax Rel-syntax A I ρ = Rel[ A ^ I ] ρ
- infix 6 Rel-syntax
-
- -- The type of arbitrarily multisorted relations of arbitrary arity
- REL : (I : ar) → (I → Type α) → {ρ : Level} → Type (𝓥 ⊔ α ⊔ suc ρ)
- REL I 𝒜 {ρ} = ((i : I) → 𝒜 i) → Type ρ
-
- REL-syntax : (I : ar) → (I → Type α) → {ρ : Level} → Type (𝓥 ⊔ α ⊔ suc ρ)
- REL-syntax I 𝒜 {ρ} = REL I 𝒜 {ρ}
-
- syntax REL-syntax I (λ i → 𝒜) = REL[ i ∈ I ] 𝒜
- infix 6 REL-syntax
-
-
- -#### Compatibility with general relations - -
-
- -- Lift a relation of tuples up to a relation on tuples of tuples.
- eval-Rel : {I : ar}{A : Type α} → Rel A I{ρ} → (J : ar) → (I → J → A) → Type (𝓥 ⊔ ρ)
- eval-Rel R J t = ∀ (j : J) → R λ i → t i j
-
-
- -A relation `R` is compatible with an operation `f` if for every tuple `t` of tuples -belonging to `R`, the tuple whose elements are the result of applying `f` to -sections of `t` also belongs to `R`. - -
-
- compatible-Rel : {I J : ar}{A : Type α} → Op(A) J → Rel A I{ρ} → Type (𝓥 ⊔ α ⊔ ρ)
- compatible-Rel f R  = ∀ t → eval-Rel R arity[ f ] t → R λ i → f (t i)
- -- (inferred type of t is I → J → A)
-
-
- - -#### Compatibility of operations with dependent relations - -
-
- eval-REL :  {I J : ar}{𝒜 : I → Type α}
-  →          REL I 𝒜 {ρ}          -- the relation type: subsets of Π[ i ∈ I ] 𝒜 i
-                                  -- (where Π[ i ∈ I ] 𝒜 i is a type of dependent functions or "tuples")
-  →          ((i : I) → J → 𝒜 i)  -- an I-tuple of (𝒥 i)-tuples
-  →          Type (𝓥 ⊔ ρ)
-
- eval-REL{I = I}{J}{𝒜} R t = ∀ j → R λ i → (t i) j
-
- compatible-REL :  {I J : ar}{𝒜 : I → Type α}
-  →                (∀ i → Op (𝒜 i) J)  -- for each i : I, an operation of type  Op(𝒜 i){J} = (J → 𝒜 i) → 𝒜 i
-  →                REL I 𝒜 {ρ}         -- a subset of Π[ i ∈ I ] 𝒜 i
-                                       -- (where Π[ i ∈ I ] 𝒜 i is a type of dependent functions or "tuples")
-  →                Type (𝓥 ⊔ α ⊔ ρ)
- compatible-REL {I = I}{J}{𝒜} 𝑓 R  = Π[ t ∈ ((i : I) → J → 𝒜 i) ] eval-REL R t
-
-
- -The definition `eval-REL` denotes an *evaluation* function which lifts an `I`-ary relation to an `(I → J)`-ary relation. - -The lifted relation will relate an `I`-tuple of `J`-tuples when the `I`-slices (or rows) of the `J`-tuples belong -to the original relation. - -The second definition, compatible-REL, denotes compatibility of an operation with a continuous relation. - - -#### Detailed explanation of the dependent relation type - -The last two definitions above may be hard to comprehend at first, so perhaps a more detailed explanation of the semantics of these deifnitions would help. - -First, one should internalize the fact that `𝒶 : I → J → A` denotes an `I`-tuple of `J`-tuples of inhabitants of `A`. - -Next, recall that a continuous relation `R` denotes a certain collection of `I`-tuples (if `x : I → A`, then `R x` asserts that `x` belongs to `R`). - -For such `R`, the type `eval-REL R` represents a certain collection of `I`-tuples of `J`-tuples, namely, the tuples `𝒶 : I → J → A` for which `eval-REL R 𝒶` holds. - -For simplicity, pretend for a moment that `J` is a finite set, say, `{1, 2, ..., J}`, so that we can write down a couple of the `J`-tuples as columns. - -For example, here are the i-th and k-th columns (for some `i k : I`). - -``` -𝒶 i 1 𝒶 k 1 -𝒶 i 2 𝒶 k 2 <-- (a row of I such columns forms an I-tuple) - ⋮ ⋮ -𝒶 i J 𝒶 k J -``` - -Now `eval-REL R 𝒶` is defined by `∀ j → R (λ i → 𝒶 i j)` which asserts that each row of the `I` columns shown above belongs to the original relation `R`. - -Finally, `compatible-REL` takes - -* an `I`-tuple (`λ i → (𝑓 i)`) of `J`-ary operations, where for each i the type of `𝑓 i` is `(J → 𝒜 i) → 𝒜 i`, and -* an `I`-tuple (`𝒶 : I → J → A`) of `J`-tuples - -and determines whether the `I`-tuple `λ i → (𝑓 i) (𝑎 i)` belongs to `R`. - --------------------------------------- - -[← Base.Relations.Discrete](Base.Relations.Discrete.html) -[Base.Relations.Properties →](Base.Relations.Properties.html) - -{% include UALib.Links.md %} - -[agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team diff --git a/docs/Overture.Basic.tex b/docs/Overture.Basic.tex deleted file mode 100644 index 256a9a6..0000000 --- a/docs/Overture.Basic.tex +++ /dev/null @@ -1,294 +0,0 @@ ---- -layout: default -title : "Overture.Basic module" -date : "2021-01-13" -author: "the agda-algebras development team" ---- - -### Preliminaries - -This is the [Overture.Basic][] module of the [Agda Universal Algebra Library][]. - -#### Logical foundations - -(See also the Equality module of the [agda-algebras][] library.) - -An Agda program typically begins by setting some options and by importing types -from existing Agda libraries. Options are specified with the `OPTIONS` *pragma* -and control the way Agda behaves by, for example, specifying the logical axioms -and deduction rules we wish to assume when the program is type-checked to verify -its correctness. Every Agda program in [agda-algebras][] begins with the following line. - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-
- -These options control certain foundational assumptions that Agda makes when -type-checking the program to verify its correctness. - -* `--without-K` disables - [Streicher's K axiom](https://ncatlab.org/nlab/show/axiom+K+%28type+theory%29); - see also the - [section on axiom K](https://agda.readthedocs.io/en/v2.6.1/language/without-k.html) - in the [Agda Language Reference Manual](https://agda.readthedocs.io/en/v2.6.1.3/language). - -* `--exact-split` makes Agda accept only those definitions that behave like so-called - *judgmental* equalities. [Martín Escardó](https://www.cs.bham.ac.uk/~mhe) explains - this by saying it "makes sure that pattern matching corresponds to Martin-Löf - eliminators;" see also the - [Pattern matching and equality section](https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html#pattern-matching-and-equality) - of the [Agda Tools](https://agda.readthedocs.io/en/v2.6.1.3/tools/) documentation. - -* `safe` ensures that nothing is postulated outright---every non-MLTT axiom has to be - an explicit assumption (e.g., an argument to a function or module); see also - [this section](https://agda.readthedocs.io/en/v2.6.1/tools/command-line-options.html#cmdoption-safe) - of the [Agda Tools](https://agda.readthedocs.io/en/v2.6.1.3/tools/) documentation and the - [Safe Agda section](https://agda.readthedocs.io/en/v2.6.1/language/safe-agda.html#safe-agda) - of the [Agda Language Reference](https://agda.readthedocs.io/en/v2.6.1.3/language). - -Note that if we wish to type-check a file that imports another file that still -has some unmet proof obligations, we must replace the `--safe` flag with -`--allow-unsolved-metas`, but this is never done in (publicly released versions - of) the [agda-algebras][]. - - -#### Agda modules - -The `OPTIONS` pragma is usually followed by the start of a module. For example, -the [Base.Functions.Basic][] module begins with the following line, and then a -list of imports of things used in the module. -
-
-module Overture.Basic where
-
--- Imports from Agda and the Agda Standard Library -----------------------------------------------
-open import Agda.Primitive    using () renaming ( Set to  Type ; lzero to  ℓ₀ )
-open import Data.Product      using ( _,_ ; ∃ ; Σ-syntax ; _×_ )
-                              renaming ( proj₁ to fst ; proj₂ to snd )
-open import Function.Base     using ( _∘_ ; id )
-open import Level             using ( Level ; suc ; _⊔_ ; lift ; lower ; Lift )
-open import Relation.Binary   using ( Decidable )
-open import Relation.Binary   using ( IsEquivalence ; IsPartialOrder )
-open import Relation.Nullary  using ( Dec ; yes ; no ; Irrelevant )
-
-open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans )
-
-private variable α β : Level
-
-ℓ₁ : Level
-ℓ₁ = suc ℓ₀
-
--- the two element type
-data 𝟚 : Type ℓ₀ where 𝟎 : 𝟚 ;  𝟏 : 𝟚
-
--- the three element type
-data 𝟛 : Type ℓ₀ where 𝟎 : 𝟛 ;  𝟏 : 𝟛 ;  𝟐 : 𝟛
-
- -#### Projection notation - -The definition of `Σ` (and thus, of `×`) includes the fields `proj₁` and `proj₂` -representing the first and second projections out of the product. However, we -prefer the shorter names `fst` and `snd`. Sometimes we prefer to denote these -projections by `∣_∣` and `∥_∥`, respectively. We define these alternative -notations for projections out of pairs as follows. - -
-
-module _ {A : Type α }{B : A → Type β} where
-
- ∣_∣ : Σ[ x ∈ A ] B x → A
- ∣_∣ = fst
-
- ∥_∥ : (z : Σ[ a ∈ A ] B a) → B ∣ z ∣
- ∥_∥ = snd
-
- infix  40 ∣_∣
-
-
- -Here we put the definitions inside an *anonymous module*, which starts with the - `module` keyword followed by an underscore (instead of a module name). The -purpose is simply to move the postulated typing judgments---the "parameters" -of the module (e.g., `A : Type α`)---out of the way so they don't obfuscate -the definitions inside the module. - -Let's define some useful syntactic sugar that will make it easier to apply -symmetry and transitivity of `≡` in proofs. - -
-
-_⁻¹ : {A : Type α} {x y : A} → x ≡ y → y ≡ x
-p ⁻¹ = sym p
-
-infix  40 _⁻¹
-
-
- -If we have a proof `p : x ≡ y`, and we need a proof of `y ≡ x`, then instead of -`sym p` we can use the more intuitive `p ⁻¹`. Similarly, the following syntactic -sugar makes abundant appeals to transitivity easier to stomach. - -
-
-_∙_ : {A : Type α}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
-p ∙ q = trans p q
-
-𝑖𝑑 : (A : Type α ) → A → A
-𝑖𝑑 A = λ x → x
-
-infixl 30 _∙_
-
- -#### Sigma types - -
-
-infix 2 ∃-syntax
-
-∃-syntax : ∀ {A : Type α} → (A → Type β) → Set (α ⊔ β)
-∃-syntax = ∃
-
-syntax ∃-syntax (λ x → B) = ∃[ x ∈ A ] B
-
- -#### Pi types - -The dependent function type is traditionally denoted with an uppercase pi symbol -and typically expressed as `Π(x : A) B x`, or something similar. In Agda syntax, -one writes `(x : A) → B x` for this dependent function type, but we can define -syntax that is closer to standard notation as follows. - -
-
-Π : {A : Type α } (B : A → Type β ) → Type (α ⊔ β)
-Π {A = A} B = (x : A) → B x
-
-Π-syntax : (A : Type α)(B : A → Type β) → Type (α ⊔ β)
-Π-syntax A B = Π B
-
-syntax Π-syntax A (λ x → B) = Π[ x ∈ A ] B
-infix 6 Π-syntax
-
-
-In the modules that follow, we will see many examples of this syntax in action. - - -#### Agda's universe hierarchy - -The hierarchy of universes in Agda is structured as follows: -```agda - -Type α : Type (lsuc α) , Type (lsuc α) : Type (lsuc (lsuc α)) , etc. - -``` -and so on. This means that the universe `Type α` has type `Type(lsuc α)`, and -`Type(lsuc α)` has type `Type(lsuc (lsuc α))`, and so on. It is important to -note, however, this does *not* imply that `Type α : Type(lsuc(lsuc α))`. In other -words, Agda's universe hierarchy is *non-cumulative*. This makes it possible to -treat universe levels more precisely, which is nice. On the other hand, a -non-cumulative hierarchy can sometimes make for a non-fun proof assistant. -Specifically, in certain situations, the non-cumulativity makes it unduly -difficult to convince Agda that a program or proof is correct. - - -#### Lifting and lowering - -Here we describe a general `Lift` type that help us overcome the technical issue -described in the previous subsection. In the [Lifts of algebras -section](Base.Algebras.Basic.html#lifts-of-algebras) of the -[Base.Algebras.Basic][] module we will define a couple domain-specific lifting -types which have certain properties that make them useful for resolving universe -level problems when working with algebra types. - -Let us be more concrete about what is at issue here by considering a typical -example. Agda will often complain with errors like the following: -``` -Birkhoff.lagda:498,20-23 -α != 𝓞 ⊔ 𝓥 ⊔ (lsuc α) when checking that the expression... has type... -``` -This error message means that Agda encountered the universe level `lsuc α`, on -line 498 (columns 20--23) of the file `Birkhoff.lagda`, but was expecting a type -at level `𝓞 ⊔ 𝓥 ⊔ lsuc α` instead. - -The general `Lift` record type that we now describe makes such problems easier to -deal with. It takes a type inhabiting some universe and embeds it into a higher -universe and, apart from syntax and notation, it is equivalent to the `Lift` type -one finds in the `Level` module of the [Agda Standard Library][]. -```agda -record Lift {𝓦 α : Level} (A : Set α) : Set (α ⊔ 𝓦) where -``` -```agda - constructor lift -``` -```agda - field lower : A -``` -The point of having a ramified hierarchy of universes is to avoid Russell's -paradox, and this would be subverted if we were to lower the universe of a type -that wasn't previously lifted. However, we can prove that if an application of -`lower` is immediately followed by an application of `lift`, then the result is -the identity transformation. Similarly, `lift` followed by `lower` is the -identity. -
-
-lift∼lower : {A : Type α} → lift ∘ lower ≡ 𝑖𝑑 (Lift β A)
-lift∼lower = refl
-
-lower∼lift : {A : Type α} → (lower {α}{β}) ∘ lift ≡ 𝑖𝑑 A
-lower∼lift = refl
-
-
-The proofs are trivial. Nonetheless, we'll come across some holes these lemmas can fill. - - -#### Pointwise equality of dependent functions - -We conclude this module with a definition that conveniently represents te assertion -that two functions are (extensionally) the same in the sense that they produce -the same output when given the same input. (We will have more to say about -this notion of equality in the [Base.Equality.Extensionality][] module.) -
-
-module _ {α : Level}{A : Type α}{β : Level}{B : A → Type β } where
-
- _≈_ :  (f g : (a : A) → B a) → Type (α ⊔ β)
- f ≈ g = ∀ x → f x ≡ g x
-
- infix 8 _≈_
-
- ≈IsEquivalence : IsEquivalence _≈_
- IsEquivalence.refl   ≈IsEquivalence          = λ _ → refl
- IsEquivalence.sym    ≈IsEquivalence f≈g      = λ x → sym (f≈g x)
- IsEquivalence.trans  ≈IsEquivalence f≈g g≈h  = λ x → trans (f≈g x) (g≈h x)
-
-
-The following is convenient for proving two pairs of a product type are equal -using the fact that their respective components are equal. -
-
-≡-by-parts :  {A : Type α}{B : Type β}{u v : A × B}
- →            fst u ≡ fst v → snd u ≡ snd v → u ≡ v
-
-≡-by-parts refl refl = refl
-
-
-Lastly, we will use the following type (instead of `subst`) to transport equality -proofs. - -
-
-transport : {A : Type α } (B : A → Type β) {x y : A} → x ≡ y → B x → B y
-transport B refl = id
-
- ------------------------------- - -[← Overture.Preface](Overture.Preface.html) -[Overture.Signatures →](Overture.Signatures.html) - -{% include UALib.Links.md %} - - diff --git a/docs/Overture.Operations.tex b/docs/Overture.Operations.tex deleted file mode 100644 index 2ba67f3..0000000 --- a/docs/Overture.Operations.tex +++ /dev/null @@ -1,68 +0,0 @@ ---- -layout: default -title : "Overture.Operations module (The Agda Universal Algebra Library)" -date : "2022-06-17" -author: "the agda-algebras development team" ---- - -### Operations - -This is the [Overture.Operations][] module of the [Agda Universal Algebra Library][]. - -For consistency and readability, we reserve two universe variables for special -purposes. - -The first of these is `𝓞` which we used in the [Overture.Signatures][] -as the universe of the type of *operation symbols* of a signature. - -The second is `𝓥` which we reserve for types representing *arities* of relations or operations. - -The type `Op` encodes the arity of an operation as an arbitrary type `I : Type 𝓥`, -which gives us a very general way to represent an operation as a function type with -domain `I → A` (the type of "tuples") and codomain `A`. - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-module Overture.Operations where
-
--- Imports from Agda and the Agda Standard Library -----------------------------
-open import Agda.Primitive               using () renaming ( Set to Type )
-open import Level                        using ( Level ; _⊔_ )
-
-private variable α β ρ 𝓥 : Level
-
--- The type of operations on A of arity I
-Op : Type α → Type 𝓥 → Type (α ⊔ 𝓥)
-Op A I = (I → A) → A
-
-
- -For example, the `I`-*ary projection operations* on `A` are represented as inhabitants of the type `Op A I` as follows. - -
-
--- Example (projections)
-π : {I : Type 𝓥} {A : Type α } → I → Op A I
-π i = λ x → x i
-
-
- -Occasionally we want to extract the arity of a given operation symbol. - -
-
--- return the arity of a given operation symbol
-arity[_] : {I : Type 𝓥} {A : Type α } → Op A I → Type 𝓥
-arity[_] {I = I} f = I
-
- ------------ - -[← Overture.Signatures](Overture.Signatures.html) -[Base →](Base.html) - - -{% include UALib.Links.md %} - diff --git a/docs/Overture.Preface.tex b/docs/Overture.Preface.tex deleted file mode 100644 index 4b2ee08..0000000 --- a/docs/Overture.Preface.tex +++ /dev/null @@ -1,203 +0,0 @@ ---- -layout: default -title : "Overture.Preface module (The Agda Universal Algebra Library)" -date : "2021-01-14" -author: "the agda-algebras development team" ---- - -### Preface - -This is the [Overture.Preface][] module of the [Agda Universal Algebra Library][]. - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-module Overture.Preface where
-
-
- -To support formalization in type theory of research level mathematics in universal -algebra and related fields, we present the [Agda Universal Algebra -Library][] (or [agda-algebras][] for short), a library for -the [Agda][] proof assistant which contains definitions, theorems and proofs from -the foundations of universal algebra. In particular, the library formalizes the -First (Noether) Isomorphism Theorem and the [Birkhoff HSP -Theorem](https://ualib.org/Setoid.Varieties.HSP.html#proof-of-the-hsp-theorem) -asserting that every variety is an equational class. - -#### Vision and goals - -The idea for the [agda-algebras][] project originated with the observation that, -on the one hand a number of basic and important constructs in universal algebra -can be defined recursively, and theorems about them proved inductively, while on -the other hand the *types* -(of type theory---in particular, [dependent types][] and [inductive types][]) -make possible elegant formal representations of recursively defined objects, and -constructive (*computable*) proofs of their properties. These observations suggest -that there is much to gain from implementing universal algebra in a language that -facilitates working with dependent and inductive types. - -##### Primary goals - -The first goal of [agda-algebras][] is to demonstrate that it is possible to -express the foundations of universal algebra in type theory and to formalize (and -formally verify) the foundations in the Agda programming language. We will -formalize a substantial portion of the edifice on which our own mathematical -research depends, and demonstrate that our research can also be expressed in type -theory and formally implemented in such a way that we and other working -mathematicians can understand and verify the results. The resulting library will -also serve to educate our peers, and encourage and help them to formally verify -their own mathematics research. - -Our field is deep and wide and codifying all of its foundations may seem like a -daunting task and a possibly risky investment of time and energy. However, we -believe our subject is well served by a new, modern, -[constructive](https://ncatlab.org/nlab/show/constructive+mathematics) -presentation of its foundations. Our new presentation expresses the foundations -of universal algebra in the language of type theory, and uses the Agda proof -assistant to codify and formally verify everything. - -##### Secondary goals - -We wish to emphasize that our ultimate objective is not merely to translate -existing results into a more modern and formal language. Indeed, one important -goal is to develop a system that is useful for conducting research in mathematics, -and that is how we intend to use our library once we have achieved our immediate -objective of implementing the basic foundational core of universal algebra in -Agda. - -To this end, our long-term objectives include - -+ domain specific types to express the idioms of universal algebra, -+ automated proof search for universal algebra, and -+ formalization of theorems discovered in our own (informal) mathematics research, -+ documentation of the resulting Agda library so it is usable by others. - -For our own mathematics research, we believe a proof assistant like Agda, equipped -with a specialized library for universal algebra is an extremely useful research -tool. Thus, a secondary goal is to demonstrate (to ourselves and colleagues) the -utility of such technologies for discovering new mathematics. - -#### Logical foundations - -The [Agda Universal Algebra Library][] is based on a minimal version of -[Martin-Löf dependent type theory][] (MLTT) as implemented in Agda. More details -on this type theory can be read at [ncatlab entry on Martin-Löf dependent type -theory](https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory). - - -#### Intended audience - -The comments and source code in the library should provide enough detail so that -people familiar with functional programming and proof assistants can learn enough -about Agda and its libraries to put them to use when creating, formalizing, and -verifying mathematical theorems and proofs. - -While there are no strict prerequisites, we expect anyone with an interest in this -work will have been motivated by prior exposure to universal algebra, as presented -in, say, [Bergman (2012)][] or [McKenzie, McNulty, Taylor (2018)], or category -theory, as presented in, say, [Riehl (2017)][]. - -Some prior exposure to [type theory][] and Agda would be helpful, but even without -this background one might still be able to get something useful out of this by -referring to one or more of the resources mentioned in the references section -below to fill in gaps as needed. - - -#### Attributions - -##### The agda-algebras development team - -The [agda-algebras][] library is developed and maintained by the *Agda Algebras -Development Team* led by [William DeMeo][] with major contributions by senior -advisor [Jacques Carette][] (McMaster University). - -##### Acknowledgements - -We thank [Andreas Abel][], [Andrej Bauer][], [Clifford Bergman][], [Venanzio -Capretta][], [Martín Escardó][], [Ralph Freese][], [Hyeyoung Shin][], and [Siva -Somayyajula][] for helpful discussions, corrections, advice, inspiration and -encouragement. - -Most of the mathematical results formalized in the [agda-algebras][] -are well known. Regarding the source code in the [agda-algebras][] -library, this is mainly due to the contributors listed above. - - -#### References - -The following Agda documentation and tutorials helped inform and improve the -[agda-algebras][] library, especially the first one in the list. - -* Escardo, [Introduction to Univalent Foundations of Mathematics with Agda][] -* Wadler, [Programming Language Foundations in Agda][] -* Bove and Dybjer, [Dependent Types at Work][] -* Gunther, Gadea, Pagano, [Formalization of Universal Algebra in Agda][] -* Norell and Chapman, [Dependently Typed Programming in Agda][] - -Finally, the official [Agda Wiki][], [Agda User's Manual][], [Agda Language -Reference][], and the (open source) [Agda Standard Library][] source code are also -quite useful. - - -#### Citing the agda-algebras library - -If you find the [agda-algebras][] library useful, please cite it using the -following BibTeX entry: - -```bibtex -@misc{ualib_v2.0.1, - author = {De{M}eo, William and Carette, Jacques}, - title = {The {A}gda {U}niversal {A}lgebra {L}ibrary (agda-algebras)}, - year = 2021, - note = {Documentation available at https://ualib.org}, - version = {2.0.1}, - doi = {10.5281/zenodo.5765793}, - howpublished = {Git{H}ub.com}, - note = {Ver.~2.0.1; source code: - \href{https://zenodo.org/record/5765793/files/ualib/agda-algebras-v.2.0.1.zip?download=1} - {agda-algebras-v.2.0.1.zip}, {G}it{H}ub repo: - \href{https://github.com/ualib/agda-algebras}{github.com/ualib/agda-algebras}} -} -``` - -#### Citing the formalization of Birkhoff's Theorem - -To cite the [formalization of Birkhoff's HSP -Theorem](https://ualib.org/Setoid.Varieties.HSP.html#proof-of-the-hsp-theorem), -please use the following BibTeX entry: - -```bibtex -@article{DeMeo:2021, - author = {De{M}eo, William and Carette, Jacques}, - title = {A {M}achine-checked {P}roof of {B}irkhoff's {V}ariety {T}heorem - in {M}artin-{L}\"of {T}ype {T}heory}, - journal = {CoRR}, - volume = {abs/2101.10166}, - year = {2021}, - eprint = {2101.2101.10166}, - archivePrefix = {arXiv}, - primaryClass = {cs.LO}, - url = {https://arxiv.org/abs/2101.10166}, - note = {Source code: - \href{https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda} - {https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda}} -} -``` - - -#### Contributions welcomed - -Readers and users are encouraged to suggest improvements to the Agda -[agda-algebras][] library and/or its documentation by submitting a -[new issue](https://github.com/ualib/agda-algebras/issues/new/choose) or -[merge request](https://github.com/ualib/agda-algebras/compare) to -[github.com/ualib/agda-algebras/](https://github.com/ualib/agda-algebras). - ------------------------------------------------- - -[↑ Overture](Overture.html) -[Overture.Basic →](Overture.Basic.html) - -{% include UALib.Links.md %} diff --git a/docs/Overture.Signatures.tex b/docs/Overture.Signatures.tex deleted file mode 100644 index e70746f..0000000 --- a/docs/Overture.Signatures.tex +++ /dev/null @@ -1,123 +0,0 @@ ---- -layout: default -title : "Overture.Signatures module (Agda Universal Algebra Library)" -date : "2021-04-23" -author: "agda-algebras development team" ---- - - -### Signatures - -This is the [Overture.Signatures][] module of the [Agda Universal Algebra Library][]. - - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-module Overture.Signatures where
-
--- Imports from the Agda (Builtin) and the Agda Standard Library -----------------------
-open import Agda.Primitive  using () renaming ( Set to  Type )
-open import Data.Product    using ( Σ-syntax )
-open import Level           using ( Level ; suc ; _⊔_ )
-
-variable 𝓞 𝓥 : Level
-
-
- -The variables `𝓞` and `𝓥` are not private since, throughout the [agda-algebras][] library, -`𝓞` denotes the universe level of *operation symbol* types, while `𝓥` denotes the universe -level of *arity* types. - -#### Theoretical background - -In [model theory](https://en.wikipedia.org/wiki/Model_theory), the *signature* -`𝑆 = (𝐶, 𝐹, 𝑅, ρ)` of a structure consists of three (possibly empty) sets `𝐶`, `𝐹`, -and `𝑅`---called *constant symbols*, *function symbols*, and *relation symbols*, -respectively---along with a function `ρ : 𝐶 + 𝐹 + 𝑅 → 𝑁` that assigns an -*arity* to each symbol. - -Often (but not always) `𝑁 = ℕ`, the natural numbers. - -As our focus here is universal algebra, we are more concerned with the restricted -notion of an *algebraic signature* (or *signature* for algebraic structures), by -which we mean a pair `𝑆 = (𝐹, ρ)` consisting of a collection `𝐹` of *operation -symbols* and an *arity function* `ρ : 𝐹 → 𝑁` that maps each operation symbol to -its arity; here, 𝑁 denotes the *arity type*. - -Heuristically, the arity `ρ 𝑓` of an operation symbol `𝑓 ∈ 𝐹` may be thought of as -the "number of arguments" that `𝑓` takes as "input". - -If the arity of `𝑓` is `n`, then we call `𝑓` an `n`-*ary* operation symbol. In -case `n` is 0 (or 1 or 2 or 3, respectively) we call the function *nullary* (or -*unary* or *binary* or *ternary*, respectively). - -If `A` is a set and `𝑓` is a (`ρ 𝑓`)-ary operation on `A`, we often indicate this -by writing `𝑓 : A`ρ 𝑓 `→ A`. On the other hand, the arguments of such -an operation form a (`ρ 𝑓`)-tuple, say, `(a 0, a 1, …, a (ρf-1))`, which may be -viewed as the graph of the function `a : ρ𝑓 → A`. - -When the codomain of `ρ` is `ℕ`, we may view `ρ 𝑓` as the finite set `{0, 1, …, ρ𝑓 - 1}`. - -Thus, by identifying the `ρ𝑓`-th power `A`ρ 𝑓 with the type `ρ 𝑓 → A` of -functions from `{0, 1, …, ρ𝑓 - 1}` to `A`, we identify the type -`A`ρ f `→ A` with the function type `(ρ𝑓 → A) → A`. - -**Example**. - -Suppose `𝑔 : (m → A) → A` is an `m`-ary operation on `A`. - -Let `a : m → A` be an `m`-tuple on `A`. - -Then `𝑔 a` may be viewed as `𝑔 (a 0, a 1, …, a (m-1))`, which has type `A`. - -Suppose further that `𝑓 : (ρ𝑓 → B) → B` is a `ρ𝑓`-ary operation on `B`. - -Let `a : ρ𝑓 → A` be a `ρ𝑓`-tuple on `A`, and let `h : A → B` be a function. - -Then the following typing judgments obtain: - -`h ∘ a : ρ𝑓 → B` and `𝑓 (h ∘ a) : B`. - - - -#### The signature type - -In the [agda-algebras][] library we represent the *signature* of an algebraic -structure using the following type. - -
-
-Signature : (𝓞 𝓥 : Level) → Type (suc (𝓞 ⊔ 𝓥))
-Signature 𝓞 𝓥 = Σ[ F ∈ Type 𝓞 ] (F → Type 𝓥)
-
-
- -Occasionally it is useful to obtain the universe level of a given signature. - -
-
-Level-of-Signature : {𝓞 𝓥 : Level} → Signature 𝓞 𝓥 → Level
-Level-of-Signature {𝓞}{𝓥} _ = suc (𝓞 ⊔ 𝓥)
-
-
- -In the [Base.Functions][] module of the [agda-algebras][] library, special syntax -is defined for the first and second projections---namely, `∣_∣` and `∥_∥`, resp. - -Consequently, if `𝑆 : Signature 𝓞 𝓥` is a signature, then - -* `∣ 𝑆 ∣` denotes the set of operation symbols, and -* `∥ 𝑆 ∥` denotes the arity function. - -If `𝑓 : ∣ 𝑆 ∣` is an operation symbol in the signature `𝑆`, then `∥ 𝑆 ∥ 𝑓` is the -arity of `𝑓`. - ----------------------- - -[← Overture.Basic](Overture.Basic.html) -[Overture.Operations →](Overture.Operations.html) - - -{% include UALib.Links.md %} diff --git a/docs/Overture.tex b/docs/Overture.tex deleted file mode 100644 index cdef161..0000000 --- a/docs/Overture.tex +++ /dev/null @@ -1,29 +0,0 @@ ---- -layout: default -title : "Overture module" -date : "2022-17-06" -author: "the agda-algebras development team" ---- - -## Overture - -This is the [Overture][] module of the [Agda Universal Algebra Library][]. - -
-
-{-# OPTIONS --without-K --exact-split --safe #-}
-
-module Overture where
-
-open import Overture.Preface     public
-open import Overture.Basic       public
-open import Overture.Signatures  public
-open import Overture.Operations  public
-
- --------------------------------------- - -[↑ Top](index.html) -[Overture.Preface →](Overture.Preface.html) - -{% include UALib.Links.md %}