From 5dc1cb909dcdc0befa8ca15ee7730adc9cc85a6b Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 09:45:44 +0000 Subject: [PATCH 1/6] added `RawNNO` --- src/Algebra/Bundles/Raw.agda | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 727440d85e..566a63a238 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -13,6 +13,21 @@ open import Relation.Binary.Core using (Rel) open import Level using (suc; _⊔_) open import Relation.Nullary.Negation.Core using (¬_) +------------------------------------------------------------------------ +-- Raw bundles with 1 unary operation & 1 element +------------------------------------------------------------------------ + +-- A raw NNO is a NNO without any laws. + +record RawNNO c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 _+1# + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+1# : Op₁ Carrier + 0# : Carrier + ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation ------------------------------------------------------------------------ From 99bd01e8889cb049fe7588e4054b107d7d0521df Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 3 Feb 2024 11:05:58 +0000 Subject: [PATCH 2/6] [fix #2273] Add `NNO`-related modules --- CHANGELOG.md | 23 +++++++++++++ src/Algebra/Bundles.agda | 23 ++++++++++++- src/Algebra/Morphism/Structures.agda | 48 ++++++++++++++++++++++++++-- src/Algebra/Structures.agda | 14 ++++++++ 4 files changed, 105 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e8f0a568f2..a0d0142d54 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -46,6 +46,16 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Bundles` + ```agda + record NNO c ℓ : Set (suc (c ⊔ ℓ)) + ``` + +* In `Algebra.Bundles.Raw` + ```agda + record RawNNO c ℓ : Set (suc (c ⊔ ℓ)) + ``` + * In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. * In `Algebra.Module.Construct.DirectProduct`: @@ -84,6 +94,19 @@ Additions to existing modules rawModule : RawModule R c ℓ ``` +* In `Algebra.Morphism.Structures` + ```agda + module NNOMorphisms (N₁ : RawNNO a ℓ₁) (N₂ : RawNNO b ℓ₂) where + record IsNNOHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsNNOMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsNNOIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + ``` + +* In `Algebra.Structures` + ```agda + record IsNNO (+1# : Op₁ A) (0# : A) : Set _ + ``` + * In `Data.Fin.Properties`: ```agda nonZeroIndex : Fin n → ℕ.NonZero n diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 6b6384458a..23fc9ea2ea 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -23,11 +23,32 @@ open import Level -- Re-export definitions of 'raw' bundles open Raw public - using (RawMagma; RawMonoid; RawGroup + using ( RawNNO; RawMagma; RawMonoid; RawGroup ; RawNearSemiring; RawSemiring ; RawRingWithoutOne; RawRing ; RawQuasigroup; RawLoop; RawKleeneAlgebra) +------------------------------------------------------------------------ +-- Bundles with 1 unary operation & 1 element +------------------------------------------------------------------------ + +record NNO c ℓ : Set (suc (c ⊔ ℓ)) where + infix 8 _+1# + infix 4 _≈_ + field + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+1# : Op₁ Carrier + 0# : Carrier + isNNO : IsNNO _≈_ _+1# 0# + + open IsNNO isNNO public + + rawNNO : RawNNO _ _ + rawNNO = record { _≈_ = _≈_; _+1# = _+1#; 0# = 0# } + + open RawNNO rawNNO public + ------------------------------------------------------------------------ -- Bundles with 1 binary operation ------------------------------------------------------------------------ diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index e73fa7e9e6..5adf99ce8a 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -6,8 +6,6 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary.Core - module Algebra.Morphism.Structures where open import Algebra.Core @@ -15,12 +13,58 @@ open import Algebra.Bundles import Algebra.Morphism.Definitions as MorphismDefinitions open import Level using (Level; _⊔_) open import Function.Definitions +open import Relation.Binary.Core open import Relation.Binary.Morphism.Structures private variable a b ℓ₁ ℓ₂ : Level +------------------------------------------------------------------------ +-- Morphisms over NNO-like structures +------------------------------------------------------------------------ + +module NNOMorphisms (N₁ : RawNNO a ℓ₁) (N₂ : RawNNO b ℓ₂) where + + open RawNNO N₁ renaming (Carrier to A; _≈_ to _≈₁_; _+1# to _+1#₁; 0# to 0#₁) + open RawNNO N₂ renaming (Carrier to B; _≈_ to _≈₂_; _+1# to _+1#₂; 0# to 0#₂) + open MorphismDefinitions A B _≈₂_ + + + record IsNNOHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ + +1#-homo : Homomorphic₁ ⟦_⟧ _+1#₁ _+1#₂ + 0#-homo : Homomorphic₀ ⟦_⟧ 0#₁ 0#₂ + + record IsNNOMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + field + isNNOHomomorphism : IsNNOHomomorphism ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ + + open IsNNOHomomorphism isNNOHomomorphism public + + isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧ + isRelMonomorphism = record + { isHomomorphism = isRelHomomorphism + ; injective = injective + } + + + record IsNNOIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + field + isNNOMonomorphism : IsNNOMonomorphism ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ + + open IsNNOMonomorphism isNNOMonomorphism public + + isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧ + isRelIsomorphism = record + { isMonomorphism = isRelMonomorphism + ; surjective = surjective + } + + ------------------------------------------------------------------------ -- Morphisms over magma-like structures ------------------------------------------------------------------------ diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 44208367ea..7d41f66bff 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -27,6 +27,20 @@ import Algebra.Consequences.Setoid as Consequences open import Data.Product.Base using (_,_; proj₁; proj₂) open import Level using (_⊔_) +------------------------------------------------------------------------ +-- Structures with 1 unary operation & 1 element +------------------------------------------------------------------------ + +record IsNNO (+1# : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where + field + isEquivalence : IsEquivalence _≈_ + +1#-cong : Congruent₁ +1# + + open IsEquivalence isEquivalence public + + setoid : Setoid a ℓ + setoid = record { isEquivalence = isEquivalence } + ------------------------------------------------------------------------ -- Structures with 1 binary operation ------------------------------------------------------------------------ From 096a76e81a1be9ff6c476745c682f92b2afd76cc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 4 Feb 2024 09:40:25 +0000 Subject: [PATCH 3/6] start again, fail better... --- CHANGELOG.md | 14 ++++++------ src/Algebra/Bundles.agda | 22 +++++++++---------- src/Algebra/Bundles/Raw.agda | 4 ++-- src/Algebra/Morphism/Structures.agda | 32 ++++++++++++++++------------ src/Algebra/Structures.agda | 2 +- 5 files changed, 39 insertions(+), 35 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a0d0142d54..73e9e89ea3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,12 +48,12 @@ Additions to existing modules * In `Algebra.Bundles` ```agda - record NNO c ℓ : Set (suc (c ⊔ ℓ)) + record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) ``` * In `Algebra.Bundles.Raw` ```agda - record RawNNO c ℓ : Set (suc (c ⊔ ℓ)) + record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) ``` * In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. @@ -96,15 +96,15 @@ Additions to existing modules * In `Algebra.Morphism.Structures` ```agda - module NNOMorphisms (N₁ : RawNNO a ℓ₁) (N₂ : RawNNO b ℓ₂) where - record IsNNOHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsNNOMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsNNOIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where + record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ + record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ ``` * In `Algebra.Structures` ```agda - record IsNNO (+1# : Op₁ A) (0# : A) : Set _ + record IsSuccessorSet (+1# : Op₁ A) (0# : A) : Set _ ``` * In `Data.Fin.Properties`: diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index 23fc9ea2ea..1fdb75cb76 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -23,7 +23,7 @@ open import Level -- Re-export definitions of 'raw' bundles open Raw public - using ( RawNNO; RawMagma; RawMonoid; RawGroup + using ( RawSuccessorSet; RawMagma; RawMonoid; RawGroup ; RawNearSemiring; RawSemiring ; RawRingWithoutOne; RawRing ; RawQuasigroup; RawLoop; RawKleeneAlgebra) @@ -32,22 +32,22 @@ open Raw public -- Bundles with 1 unary operation & 1 element ------------------------------------------------------------------------ -record NNO c ℓ : Set (suc (c ⊔ ℓ)) where +record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _+1# infix 4 _≈_ field - Carrier : Set c - _≈_ : Rel Carrier ℓ - _+1# : Op₁ Carrier - 0# : Carrier - isNNO : IsNNO _≈_ _+1# 0# + Carrier : Set c + _≈_ : Rel Carrier ℓ + _+1# : Op₁ Carrier + 0# : Carrier + isSuccessorSet : IsSuccessorSet _≈_ _+1# 0# - open IsNNO isNNO public + open IsSuccessorSet isSuccessorSet public - rawNNO : RawNNO _ _ - rawNNO = record { _≈_ = _≈_; _+1# = _+1#; 0# = 0# } + rawSuccessorSet : RawSuccessorSet _ _ + rawSuccessorSet = record { _≈_ = _≈_; _+1# = _+1#; 0# = 0# } - open RawNNO rawNNO public + open RawSuccessorSet rawSuccessorSet public ------------------------------------------------------------------------ -- Bundles with 1 binary operation diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 566a63a238..92bd89a4d5 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -17,9 +17,9 @@ open import Relation.Nullary.Negation.Core using (¬_) -- Raw bundles with 1 unary operation & 1 element ------------------------------------------------------------------------ --- A raw NNO is a NNO without any laws. +-- A raw SuccessorSet is a SuccessorSet without any laws. -record RawNNO c ℓ : Set (suc (c ⊔ ℓ)) where +record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where infix 8 _+1# infix 4 _≈_ field diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 5adf99ce8a..26a33ca250 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -21,28 +21,32 @@ private a b ℓ₁ ℓ₂ : Level ------------------------------------------------------------------------ --- Morphisms over NNO-like structures +-- Morphisms over SuccessorSet-like structures ------------------------------------------------------------------------ -module NNOMorphisms (N₁ : RawNNO a ℓ₁) (N₂ : RawNNO b ℓ₂) where +module SuccessorSetMorphisms + (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) + where - open RawNNO N₁ renaming (Carrier to A; _≈_ to _≈₁_; _+1# to _+1#₁; 0# to 0#₁) - open RawNNO N₂ renaming (Carrier to B; _≈_ to _≈₂_; _+1# to _+1#₂; 0# to 0#₂) + open RawSuccessorSet N₁ + renaming (Carrier to A; _≈_ to _≈₁_; _+1# to _+1#₁; 0# to 0#₁) + open RawSuccessorSet N₂ + renaming (Carrier to B; _≈_ to _≈₂_; _+1# to _+1#₂; 0# to 0#₂) open MorphismDefinitions A B _≈₂_ - - record IsNNOHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + + record IsSuccessorSetHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ +1#-homo : Homomorphic₁ ⟦_⟧ _+1#₁ _+1#₂ 0#-homo : Homomorphic₀ ⟦_⟧ 0#₁ 0#₂ - record IsNNOMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where + record IsSuccessorSetMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field - isNNOHomomorphism : IsNNOHomomorphism ⟦_⟧ - injective : Injective _≈₁_ _≈₂_ ⟦_⟧ + isSuccessorSetHomomorphism : IsSuccessorSetHomomorphism ⟦_⟧ + injective : Injective _≈₁_ _≈₂_ ⟦_⟧ - open IsNNOHomomorphism isNNOHomomorphism public + open IsSuccessorSetHomomorphism isSuccessorSetHomomorphism public isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelMonomorphism = record @@ -51,12 +55,12 @@ module NNOMorphisms (N₁ : RawNNO a ℓ₁) (N₂ : RawNNO b ℓ₂) where } - record IsNNOIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where + record IsSuccessorSetIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field - isNNOMonomorphism : IsNNOMonomorphism ⟦_⟧ - surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ + isSuccessorSetMonomorphism : IsSuccessorSetMonomorphism ⟦_⟧ + surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧ - open IsNNOMonomorphism isNNOMonomorphism public + open IsSuccessorSetMonomorphism isSuccessorSetMonomorphism public isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧ isRelIsomorphism = record diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 7d41f66bff..68c15b446d 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -31,7 +31,7 @@ open import Level using (_⊔_) -- Structures with 1 unary operation & 1 element ------------------------------------------------------------------------ -record IsNNO (+1# : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where +record IsSuccessorSet (+1# : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where field isEquivalence : IsEquivalence _≈_ +1#-cong : Congruent₁ +1# From 45d5ab7b2749e19f81908fe1f9fd01103178a0fc Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 11 Feb 2024 05:06:43 +0000 Subject: [PATCH 4/6] rectify names --- src/Algebra/Bundles.agda | 9 ++++----- src/Algebra/Bundles/Raw.agda | 5 ++--- src/Algebra/Morphism/Structures.agda | 8 ++++---- src/Algebra/Structures.agda | 4 ++-- 4 files changed, 12 insertions(+), 14 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index ada485f66b..a255b62d18 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -33,19 +33,18 @@ open Raw public ------------------------------------------------------------------------ record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where - infix 8 _+1# infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ - _+1# : Op₁ Carrier - 0# : Carrier - isSuccessorSet : IsSuccessorSet _≈_ _+1# 0# + suc# : Op₁ Carrier + zero# : Carrier + isSuccessorSet : IsSuccessorSet _≈_ suc# zero# open IsSuccessorSet isSuccessorSet public rawSuccessorSet : RawSuccessorSet _ _ - rawSuccessorSet = record { _≈_ = _≈_; _+1# = _+1#; 0# = 0# } + rawSuccessorSet = record { _≈_ = _≈_; suc# = suc#; zero# = zero# } open RawSuccessorSet rawSuccessorSet public diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda index 92bd89a4d5..5c99d02790 100644 --- a/src/Algebra/Bundles/Raw.agda +++ b/src/Algebra/Bundles/Raw.agda @@ -20,13 +20,12 @@ open import Relation.Nullary.Negation.Core using (¬_) -- A raw SuccessorSet is a SuccessorSet without any laws. record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where - infix 8 _+1# infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ - _+1# : Op₁ Carrier - 0# : Carrier + suc# : Op₁ Carrier + zero# : Carrier ------------------------------------------------------------------------ -- Raw bundles with 1 binary operation diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda index 26a33ca250..c352904be7 100644 --- a/src/Algebra/Morphism/Structures.agda +++ b/src/Algebra/Morphism/Structures.agda @@ -29,17 +29,17 @@ module SuccessorSetMorphisms where open RawSuccessorSet N₁ - renaming (Carrier to A; _≈_ to _≈₁_; _+1# to _+1#₁; 0# to 0#₁) + renaming (Carrier to A; _≈_ to _≈₁_; suc# to suc#₁; zero# to zero#₁) open RawSuccessorSet N₂ - renaming (Carrier to B; _≈_ to _≈₂_; _+1# to _+1#₂; 0# to 0#₂) + renaming (Carrier to B; _≈_ to _≈₂_; suc# to suc#₂; zero# to zero#₂) open MorphismDefinitions A B _≈₂_ record IsSuccessorSetHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧ - +1#-homo : Homomorphic₁ ⟦_⟧ _+1#₁ _+1#₂ - 0#-homo : Homomorphic₀ ⟦_⟧ 0#₁ 0#₂ + suc#-homo : Homomorphic₁ ⟦_⟧ suc#₁ suc#₂ + zero#-homo : Homomorphic₀ ⟦_⟧ zero#₁ zero#₂ record IsSuccessorSetMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where field diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 68c15b446d..95f57d8c6a 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -31,10 +31,10 @@ open import Level using (_⊔_) -- Structures with 1 unary operation & 1 element ------------------------------------------------------------------------ -record IsSuccessorSet (+1# : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where +record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set (a ⊔ ℓ) where field isEquivalence : IsEquivalence _≈_ - +1#-cong : Congruent₁ +1# + suc#-cong : Congruent₁ suc# open IsEquivalence isEquivalence public From 491b65438bd2cedc863bce9d1ca9a1af1dc5d02c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 11 Feb 2024 05:07:43 +0000 Subject: [PATCH 5/6] tighten `import`s --- src/Algebra/Bundles.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda index a255b62d18..1969731c2c 100644 --- a/src/Algebra/Bundles.agda +++ b/src/Algebra/Bundles.agda @@ -15,8 +15,6 @@ import Algebra.Bundles.Raw as Raw open import Algebra.Core open import Algebra.Structures open import Relation.Binary.Core using (Rel) -open import Function.Base -import Relation.Nullary as N open import Level ------------------------------------------------------------------------ From 84964ff423243af007733ee98e131fd99f7dcfdf Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 11 Feb 2024 05:11:42 +0000 Subject: [PATCH 6/6] rectify names: `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 76789be49b..2567d8b204 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -129,7 +129,7 @@ Additions to existing modules * In `Algebra.Structures` ```agda - record IsSuccessorSet (+1# : Op₁ A) (0# : A) : Set _ + record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ ``` * In `Data.Fin.Properties`: