Skip to content

Commit 2c653ae

Browse files
fredrik-bakkefredrik-bakke
authored
Refactor universal-algebra (#1657)
1 parent 91f2e48 commit 2c653ae

23 files changed

+1245
-989
lines changed

‎config/codespell-dictionary.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ cagegory->category
2020
characteriation->characterization
2121
characteriing->characterizing
2222
conceot->concept
23+
congruece->congruence
24+
congrueces->congruences
2325
conisist->consist
2426
conisisted->consisted
2527
conisisting->consisting

‎docs/tables/categories.md‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,22 @@
1-
| Category | File |
2-
| ---------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
3-
| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) |
4-
| Algebras over an equational theory | [`universal-algebra.category-of-algebras-of-theories`](universal-algebra.category-of-algebras-of-theories.md) |
5-
| Commutative rings | [`commutative-algebra.category-of-commutative-rings`](commutative-algebra.category-of-commutative-rings.md) |
6-
| Connected set bundles over 𝕊¹ | [`synthetic-homotopy-theory.category-of-connected-set-bundles-circle`](synthetic-homotopy-theory.category-of-connected-set-bundles-circle.md) |
7-
| Copresheaves on a precategory | [`category-theory.copresheaf-categories`](category-theory.copresheaf-categories.md) |
8-
| Cyclic rings | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md) |
9-
| Functors between two categories | [`category-theory.category-of-functors`](category-theory.category-of-functors.md) [`category-theory.category-of-functors-from-small-to-large-categories`](category-theory.category-of-functors-from-small-to-large-categories.md) |
10-
| Families of sets | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md) |
11-
| Groups | [`group-theory.category-of-groups`](group-theory.category-of-groups.md) |
12-
| `G`-sets | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md) |
13-
| Maps between two categories | [`category-theory.category-of-maps-categories`](category-theory.category-of-maps-categories.md) [`category-theory.category-of-maps-from-small-to-large-categories`](category-theory.category-of-maps-from-small-to-large-categories.md) |
14-
| Metric spaces and isometries | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md) |
15-
| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md) |
16-
| Orbits of a group | [`group-theory.category-of-orbits-groups`](group-theory.category-of-orbits-groups.md) |
17-
| Presheaves on a precategory | [`category-theory.presheaf-categories`](category-theory.presheaf-categories.md) |
18-
| Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) |
19-
| Rings | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md) |
20-
| Semigroups | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md) |
21-
| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) |
22-
| Simplicial sets | [`category-theory.category-of-simplicial-sets`](category-theory.category-of-simplicial-sets.md) |
1+
| Category | File |
2+
| --------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
3+
| Abelian groups | [`group-theory.category-of-abelian-groups`](group-theory.category-of-abelian-groups.md) |
4+
| Algebras over an algebraic theory | [`universal-algebra.category-of-algebras-algebraic-theories`](universal-algebra.category-of-algebras-algebraic-theories.md) |
5+
| Commutative rings | [`commutative-algebra.category-of-commutative-rings`](commutative-algebra.category-of-commutative-rings.md) |
6+
| Connected set bundles over 𝕊¹ | [`synthetic-homotopy-theory.category-of-connected-set-bundles-circle`](synthetic-homotopy-theory.category-of-connected-set-bundles-circle.md) |
7+
| Copresheaves on a precategory | [`category-theory.copresheaf-categories`](category-theory.copresheaf-categories.md) |
8+
| Cyclic rings | [`ring-theory.category-of-cyclic-rings`](ring-theory.category-of-cyclic-rings.md) |
9+
| Functors between two categories | [`category-theory.category-of-functors`](category-theory.category-of-functors.md) [`category-theory.category-of-functors-from-small-to-large-categories`](category-theory.category-of-functors-from-small-to-large-categories.md) |
10+
| Families of sets | [`foundation.category-of-families-of-sets`](foundation.category-of-families-of-sets.md) |
11+
| Groups | [`group-theory.category-of-groups`](group-theory.category-of-groups.md) |
12+
| `G`-sets | [`group-theory.category-of-group-actions`](group-theory.category-of-group-actions.md) |
13+
| Maps between two categories | [`category-theory.category-of-maps-categories`](category-theory.category-of-maps-categories.md) [`category-theory.category-of-maps-from-small-to-large-categories`](category-theory.category-of-maps-from-small-to-large-categories.md) |
14+
| Metric spaces and isometries | [`metric-spaces.category-of-metric-spaces-and-isometries`](metric-spaces.category-of-metric-spaces-and-isometries.md) |
15+
| Metric spaces and short functions | [`metric-spaces.category-of-metric-spaces-and-short-functions`](metric-spaces.category-of-metric-spaces-and-short-functions.md) |
16+
| Orbits of a group | [`group-theory.category-of-orbits-groups`](group-theory.category-of-orbits-groups.md) |
17+
| Presheaves on a precategory | [`category-theory.presheaf-categories`](category-theory.presheaf-categories.md) |
18+
| Representing arrow category | [`category-theory.representing-arrow-category`](category-theory.representing-arrow-category.md) |
19+
| Rings | [`ring-theory.category-of-rings`](ring-theory.category-of-rings.md) |
20+
| Semigroups | [`group-theory.category-of-semigroups`](group-theory.category-of-semigroups.md) |
21+
| Sets | [`foundation.category-of-sets`](foundation.category-of-sets.md) |
22+
| Simplicial sets | [`category-theory.category-of-simplicial-sets`](category-theory.category-of-simplicial-sets.md) |

‎src/universal-algebra.lagda.md‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,17 @@ module universal-algebra where
88
open import universal-algebra.abstract-equations-over-signatures public
99
open import universal-algebra.algebraic-theories public
1010
open import universal-algebra.algebraic-theory-of-groups public
11-
open import universal-algebra.algebras-of-theories public
12-
open import universal-algebra.category-of-algebras-of-theories public
11+
open import universal-algebra.algebras public
12+
open import universal-algebra.category-of-algebras-algebraic-theories public
1313
open import universal-algebra.congruences public
14-
open import universal-algebra.equivalences-of-models-of-signatures public
14+
open import universal-algebra.equivalences-models-of-signatures public
15+
open import universal-algebra.extensions-signatures public
1516
open import universal-algebra.homomorphisms-of-algebras public
1617
open import universal-algebra.isomorphisms-of-algebras public
1718
open import universal-algebra.kernels public
1819
open import universal-algebra.models-of-signatures public
1920
open import universal-algebra.morphisms-of-models-of-signatures public
20-
open import universal-algebra.precategory-of-algebras-of-theories public
21+
open import universal-algebra.precategory-of-algebras-algebraic-theories public
2122
open import universal-algebra.quotient-algebras public
2223
open import universal-algebra.signatures public
2324
open import universal-algebra.terms-over-signatures public

‎src/universal-algebra/abstract-equations-over-signatures.lagda.md‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,13 @@ open import universal-algebra.terms-over-signatures
1919

2020
## Idea
2121

22-
An **abstract equation** over a signature `σ` is a statement of a form "`x`
23-
equals `y`", where `x` and `y` are terms over `σ`. Thus, the data of an abstract
24-
equation is simply two terms over a common signature.
22+
An
23+
{{#concept "abstract equation" Disambiguation="over a single-sorted finitary algebraic signature" Agda=abstract-equation}}
24+
over a
25+
[single-sorted finitary algebraic signature](universal-algebra.signatures.md)
26+
`σ` is a statement of the form "`x` equals `y`", where `x` and `y` are
27+
[terms](universal-algebra.terms-over-signatures.md) over `σ`. Thus, the data of
28+
an abstract equation is simply two terms over a common signature.
2529

2630
## Definitions
2731

@@ -32,12 +36,12 @@ module _
3236
{l1 : Level} (σ : signature l1)
3337
where
3438
35-
Abstract-Equation : UU l1
36-
Abstract-Equation = Term σ × Term σ
39+
abstract-equation : UU l1
40+
abstract-equation = term σ × term σ
3741
38-
lhs-Abstract-Equation : Abstract-Equation → Term σ
39-
lhs-Abstract-Equation = pr1
42+
lhs-abstract-equation : abstract-equation → term σ
43+
lhs-abstract-equation = pr1
4044
41-
rhs-Abstract-Equation : Abstract-Equation → Term σ
42-
rhs-Abstract-Equation = pr2
45+
rhs-abstract-equation : abstract-equation → term σ
46+
rhs-abstract-equation = pr2
4347
```

‎src/universal-algebra/algebraic-theories.lagda.md‎

Lines changed: 17 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -18,27 +18,32 @@ open import universal-algebra.signatures
1818

1919
## Idea
2020

21-
An algebraic theory is a collection of abstract equations over a signature `σ`
22-
that we consider to 'hold' in the theory. It is algebraic in the sense that we
23-
only require equations involving function symbols from the signature, in
21+
An
22+
{{#concept "algebraic theory" Disambiguation="single-sorted, finitary" WD="algebraic theory" WDID=Q4724020 Agda=Algebraic-Theory}}
23+
is a [collection](foundation.dependent-pair-types.md) of
24+
[abstract equations](universal-algebra.abstract-equations-over-signatures.md)
25+
over a
26+
[single-sorted finitary algebraic signature](universal-algebra.signatures.md)
27+
`σ` that we consider to 'hold' in the theory. It is algebraic in the sense that
28+
we only require equations involving function symbols from the signature, in
2429
contrast to, say, requiring additional types of relations.
2530

2631
## Definitions
2732

2833
### Theories
2934

3035
```agda
36+
Algebraic-Theory : {l1 : Level} (l2 : Level) → signature l1 → UU (l1 ⊔ lsuc l2)
37+
Algebraic-Theory l2 σ = Σ (UU l2) (λ B → (B → abstract-equation σ))
38+
3139
module _
32-
{l1 : Level} (σ : signature l1)
40+
{l1 l2 : Level} (σ : signature l1) (T : Algebraic-Theory l2 σ)
3341
where
3442
35-
Theory : (l2 : Level) → UU (l1 ⊔ lsuc l2)
36-
Theory l2 = Σ (UU l2) (λ B → (B → Abstract-Equation σ))
37-
38-
index-Theory : {l2 : Level} → Theory l2 → UU l2
39-
index-Theory = pr1
43+
index-Algebraic-Theory : UU l2
44+
index-Algebraic-Theory = pr1 T
4045
41-
index-Abstract-Equation-Theory :
42-
{l2 : Level} (Th : Theory l2) → (index-Theory Th) → Abstract-Equation σ
43-
index-Abstract-Equation-Theory Th e = pr2 Th e
46+
index-abstract-equation-Algebraic-Theory :
47+
index-Algebraic-Theory → abstract-equation σ
48+
index-abstract-equation-Algebraic-Theory = pr2 T
4449
```

0 commit comments

Comments
 (0)