Skip to content

Commit 97aa2b7

Browse files
jamesmckinnajamesmckinna
authored
Add initial+terminal algebras (#1902)
* refactored `Algebra.Construct.Zero` into `Initial` and `Terminal` * added `Algebra.Construct.Initial` and `Terminal`
1 parent 46daf81 commit 97aa2b7

File tree

7 files changed

+266
-71
lines changed

7 files changed

+266
-71
lines changed

‎CHANGELOG.md

+10
Original file line numberDiff line numberDiff line change
@@ -605,6 +605,8 @@ Non-backwards compatible changes
605605

606606
* New modules:
607607
```
608+
Algebra.Construct.Initial
609+
Algebra.Construct.Terminal
608610
Data.List.Effectful.Transformer
609611
Data.List.NonEmpty.Effectful.Transformer
610612
Data.Maybe.Effectful.Transformer
@@ -886,6 +888,14 @@ Deprecated modules
886888
Deprecated names
887889
----------------
888890

891+
* In `Algebra.Construct.Zero`:
892+
```agda
893+
rawMagma ↦ Algebra.Construct.Terminal.rawMagma
894+
magma ↦ Algebra.Construct.Terminal.magma
895+
semigroup ↦ Algebra.Construct.Terminal.semigroup
896+
band ↦ Algebra.Construct.Terminal.band
897+
```
898+
889899
* In `Codata.Guarded.Stream.Properties`:
890900
```agda
891901
map-identity ↦ map-id

‎src/Algebra/Construct/Initial.agda

+97
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances of algebraic structures where the carrier is ⊥.
5+
-- In mathematics, this is usually called 0.
6+
--
7+
-- From monoids up, these are zero-objects – i.e, the initial
8+
-- object is the terminal object in the relevant category.
9+
------------------------------------------------------------------------
10+
11+
{-# OPTIONS --without-K --safe #-}
12+
13+
open import Level using (Level)
14+
15+
module Algebra.Construct.Initial {c ℓ : Level} where
16+
17+
open import Algebra.Bundles
18+
using (Magma; Semigroup; Band)
19+
open import Algebra.Bundles.Raw
20+
using (RawMagma)
21+
open import Algebra.Core using (Op₂)
22+
open import Algebra.Definitions using (Congruent₂)
23+
open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
24+
open import Data.Empty.Polymorphic
25+
open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
26+
27+
28+
------------------------------------------------------------------------
29+
-- Re-export those algebras which are also terminal
30+
31+
open import Algebra.Construct.Terminal {c} {ℓ} public
32+
hiding (rawMagma; magma; semigroup; band)
33+
34+
------------------------------------------------------------------------
35+
-- Gather all the functionality in one place
36+
37+
module ℤero where
38+
39+
infixl 7 _∙_
40+
infix 4 _≈_
41+
42+
Carrier : Set c
43+
Carrier = ⊥
44+
45+
_≈_ : Rel Carrier ℓ
46+
_≈_ ()
47+
48+
_∙_ : Op₂ Carrier
49+
_∙_ ()
50+
51+
refl : Reflexive _≈_
52+
refl {x = ()}
53+
54+
sym : Symmetric _≈_
55+
sym {x = ()}
56+
57+
trans : Transitive _≈_
58+
trans {i = ()}
59+
60+
∙-cong : Congruent₂ _≈_ _∙_
61+
∙-cong {x = ()}
62+
63+
open ℤero
64+
65+
------------------------------------------------------------------------
66+
-- Raw bundles
67+
68+
rawMagma : RawMagma c ℓ
69+
rawMagma = record { ℤero }
70+
71+
------------------------------------------------------------------------
72+
-- Structures
73+
74+
isEquivalence : IsEquivalence _≈_
75+
isEquivalence = record { ℤero }
76+
77+
isMagma : IsMagma _≈_ _∙_
78+
isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
79+
80+
isSemigroup : IsSemigroup _≈_ _∙_
81+
isSemigroup = record { isMagma = isMagma ; assoc = λ () }
82+
83+
isBand : IsBand _≈_ _∙_
84+
isBand = record { isSemigroup = isSemigroup ; idem = λ () }
85+
86+
------------------------------------------------------------------------
87+
-- Bundles
88+
89+
magma : Magma c ℓ
90+
magma = record { isMagma = isMagma }
91+
92+
semigroup : Semigroup c ℓ
93+
semigroup = record { isSemigroup = isSemigroup }
94+
95+
band : Band c ℓ
96+
band = record { isBand = isBand }
97+

‎src/Algebra/Construct/Terminal.agda

+86
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances of algebraic structures where the carrier is ⊤.
5+
-- In mathematics, this is usually called 0 (1 in the case of Group).
6+
--
7+
-- From monoids up, these are zero-objects – i.e, both the initial
8+
-- and the terminal object in the relevant category.
9+
------------------------------------------------------------------------
10+
11+
{-# OPTIONS --without-K --safe #-}
12+
13+
open import Level using (Level)
14+
15+
module Algebra.Construct.Terminal {c ℓ : Level} where
16+
17+
open import Algebra.Bundles
18+
open import Data.Unit.Polymorphic
19+
open import Relation.Binary.Core using (Rel)
20+
21+
------------------------------------------------------------------------
22+
-- Gather all the functionality in one place
23+
24+
module 𝕆ne where
25+
26+
infix 4 _≈_
27+
Carrier : Set c
28+
Carrier = ⊤
29+
30+
_≈_ : Rel Carrier ℓ
31+
_ ≈ _ = ⊤
32+
33+
------------------------------------------------------------------------
34+
-- Raw bundles
35+
36+
rawMagma : RawMagma c ℓ
37+
rawMagma = record { 𝕆ne }
38+
39+
rawMonoid : RawMonoid c ℓ
40+
rawMonoid = record { 𝕆ne }
41+
42+
rawGroup : RawGroup c ℓ
43+
rawGroup = record { 𝕆ne }
44+
45+
rawSemiring : RawSemiring c ℓ
46+
rawSemiring = record { 𝕆ne }
47+
48+
rawRing : RawRing c ℓ
49+
rawRing = record { 𝕆ne }
50+
51+
------------------------------------------------------------------------
52+
-- Bundles
53+
54+
magma : Magma c ℓ
55+
magma = record { 𝕆ne }
56+
57+
semigroup : Semigroup c ℓ
58+
semigroup = record { 𝕆ne }
59+
60+
band : Band c ℓ
61+
band = record { 𝕆ne }
62+
63+
commutativeSemigroup : CommutativeSemigroup c ℓ
64+
commutativeSemigroup = record { 𝕆ne }
65+
66+
monoid : Monoid c ℓ
67+
monoid = record { 𝕆ne }
68+
69+
commutativeMonoid : CommutativeMonoid c ℓ
70+
commutativeMonoid = record { 𝕆ne }
71+
72+
idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
73+
idempotentCommutativeMonoid = record { 𝕆ne }
74+
75+
group : Group c ℓ
76+
group = record { 𝕆ne }
77+
78+
abelianGroup : AbelianGroup c ℓ
79+
abelianGroup = record { 𝕆ne }
80+
81+
semiring : Semiring c ℓ
82+
semiring = record { 𝕆ne }
83+
84+
ring : Ring c ℓ
85+
ring = record { 𝕆ne }
86+

‎src/Algebra/Construct/Zero.agda

+41-35
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,15 @@
22
-- The Agda standard library
33
--
44
-- Instances of algebraic structures where the carrier is ⊤.
5-
-- In mathematics, this is usually called 0.
5+
-- In mathematics, this is usually called 0 (1 in the case of Group).
66
--
77
-- From monoids up, these are are zero-objects – i.e, both the initial
88
-- and the terminal object in the relevant category.
9-
-- For structures without an identity element, we can't necessarily
10-
-- produce a homomorphism out of 0, because there is an instance of such
11-
-- a structure with an empty Carrier.
9+
--
10+
-- For structures without an identity element, the terminal algebra is
11+
-- *not* initial, because there is an instance of such a structure
12+
-- with an empty Carrier. Accordingly, such definitions are now deprecated
13+
-- in favour of those defined in `Algebra.Construct.Terminal`.
1214
------------------------------------------------------------------------
1315

1416
{-# OPTIONS --without-K --safe #-}
@@ -17,47 +19,51 @@ open import Level using (Level)
1719

1820
module Algebra.Construct.Zero {c ℓ : Level} where
1921

22+
open import Algebra.Bundles.Raw
23+
using (RawMagma)
2024
open import Algebra.Bundles
21-
open import Data.Unit.Polymorphic
25+
using (Magma; Semigroup; Band)
2226

2327
------------------------------------------------------------------------
24-
-- Raw bundles
28+
-- Re-export those algebras which are both initial and terminal
2529

26-
rawMagma : RawMagma c ℓ
27-
rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
30+
open import Algebra.Construct.Terminal public
31+
hiding (rawMagma; magma; semigroup; band)
2832

29-
rawMonoid : RawMonoid c ℓ
30-
rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
33+
------------------------------------------------------------------------
34+
-- DEPRECATED
35+
------------------------------------------------------------------------
36+
-- Please use the new definitions re-exported from
37+
-- `Algebra.Construct.Terminal` as continuing support for the below is
38+
-- not guaranteed.
3139

32-
rawGroup : RawGroup c ℓ
33-
rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
40+
-- Version 2.0
3441

35-
------------------------------------------------------------------------
36-
-- Bundles
42+
rawMagma : RawMagma c ℓ
43+
rawMagma = Algebra.Construct.Terminal.rawMagma
44+
45+
{-# WARNING_ON_USAGE rawMagma
46+
"Warning: rawMagma was deprecated in v2.0.
47+
Please use Algebra.Construct.Terminal.rawMagma instead."
48+
#-}
3749

3850
magma : Magma c ℓ
39-
magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
51+
magma = Algebra.Construct.Terminal.magma
52+
{-# WARNING_ON_USAGE magma
53+
"Warning: magma was deprecated in v2.0.
54+
Please use Algebra.Construct.Terminal.magma instead."
55+
#-}
4056

4157
semigroup : Semigroup c ℓ
42-
semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
58+
semigroup = Algebra.Construct.Terminal.semigroup
59+
{-# WARNING_ON_USAGE semigroup
60+
"Warning: semigroup was deprecated in v2.0.
61+
Please use Algebra.Construct.Terminal.semigroup instead."
62+
#-}
4363

4464
band : Band c ℓ
45-
band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
46-
47-
commutativeSemigroup : CommutativeSemigroup c ℓ
48-
commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
49-
50-
monoid : Monoid c ℓ
51-
monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
52-
53-
commutativeMonoid : CommutativeMonoid c ℓ
54-
commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
55-
56-
idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
57-
idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
58-
59-
group : Group c ℓ
60-
group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
61-
62-
abelianGroup : AbelianGroup c ℓ
63-
abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
65+
band = Algebra.Construct.Terminal.band
66+
{-# WARNING_ON_USAGE semigroup
67+
"Warning: semigroup was deprecated in v2.0.
68+
Please use Algebra.Construct.Terminal.semigroup instead."
69+
#-}

0 commit comments

Comments
 (0)