[fixes #2273] Add SuccessorSet and associated boilerplate (#2277)

* added `RawNNO`

* [fix #2273] Add `NNO`-related modules

* start again, fail better...

* rectify names

* tighten `import`s

* rectify names: `CHANGELOG`

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: 2 people

CHANGELOG.md

@@ -128,13 +128,29 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Bundles`
+  ```agda
+  record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
+  ```
+
+* In `Algebra.Bundles.Raw`
+  ```agda
+  record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ))
+  ```
+
 * Exporting more `Raw` substructures from `Algebra.Bundles.Ring`:
   ```agda
   rawNearSemiring   : RawNearSemiring _ _
   rawRingWithoutOne : RawRingWithoutOne _ _
   +-rawGroup        : RawGroup _ _
   ```
 
+* In `Algebra.Construct.Terminal`:
+  ```agda
+  rawNearSemiring : RawNearSemiring c ℓ
+  nearSemiring    : NearSemiring c ℓ
+  ```
+
 * In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
 
 * In `Algebra.Module.Construct.DirectProduct`:
@@ -173,6 +189,13 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Morphism.Structures`
+  ```agda
+  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.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
@@ -199,12 +222,6 @@ Additions to existing modules
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
 
-* In `Algebra.Construct.Terminal`:
-  ```agda
-  rawNearSemiring : RawNearSemiring c ℓ
-  nearSemiring    : NearSemiring c ℓ
-  ```
-
 * In `Algebra.Properties.Monoid.Mult`:
   ```agda
   ×-homo-0 : ∀ x → 0 × x ≈ 0#
@@ -218,6 +235,10 @@ Additions to existing modules
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
+* In `Algebra.Structures`
+  ```agda
+  record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _
+
 * In `Algebra.Structures.IsGroup`:
   ```agda
   infixl 6 _//_

src/Algebra/Bundles.agda

@@ -15,19 +15,37 @@ 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
 
 ------------------------------------------------------------------------
 -- Re-export definitions of 'raw' bundles
 
 open Raw public
-  using (RawMagma; RawMonoid; RawGroup
+  using ( RawSuccessorSet; RawMagma; RawMonoid; RawGroup
         ; RawNearSemiring; RawSemiring
         ; RawRingWithoutOne; RawRing
         ; RawQuasigroup; RawLoop; RawKleeneAlgebra)
 
+------------------------------------------------------------------------
+-- Bundles with 1 unary operation & 1 element
+------------------------------------------------------------------------
+
+record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    suc#             : Op₁ Carrier
+    zero#            : Carrier
+    isSuccessorSet   : IsSuccessorSet _≈_ suc# zero#
+
+  open IsSuccessorSet isSuccessorSet public
+
+  rawSuccessorSet : RawSuccessorSet _ _
+  rawSuccessorSet = record { _≈_ = _≈_; suc# = suc#; zero# = zero# }
+
+  open RawSuccessorSet rawSuccessorSet public
+
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation
 ------------------------------------------------------------------------

src/Algebra/Bundles/Raw.agda

@@ -13,6 +13,20 @@ 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 SuccessorSet is a SuccessorSet without any laws.
+
+record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    suc#    : Op₁ Carrier
+    zero#   : Carrier
+
 ------------------------------------------------------------------------
 -- Raw bundles with 1 binary operation
 ------------------------------------------------------------------------

src/Algebra/Morphism/Structures.agda

@@ -6,21 +6,69 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core
-
 module Algebra.Morphism.Structures where
 
 open import Algebra.Core
 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 SuccessorSet-like structures
+------------------------------------------------------------------------
+
+module SuccessorSetMorphisms
+  (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂)
+  where
+
+  open RawSuccessorSet N₁
+    renaming (Carrier to A; _≈_ to _≈₁_; suc# to suc#₁; zero# to zero#₁)
+  open RawSuccessorSet N₂
+    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 _≈₁_ _≈₂_ ⟦_⟧
+      suc#-homo         : Homomorphic₁ ⟦_⟧ suc#₁ suc#₂
+      zero#-homo        : Homomorphic₀ ⟦_⟧ zero#₁ zero#₂
+
+  record IsSuccessorSetMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isSuccessorSetHomomorphism : IsSuccessorSetHomomorphism ⟦_⟧
+      injective                  : Injective _≈₁_ _≈₂_ ⟦_⟧
+
+    open IsSuccessorSetHomomorphism isSuccessorSetHomomorphism public
+
+    isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
+    isRelMonomorphism = record
+      { isHomomorphism = isRelHomomorphism
+      ; injective      = injective
+      }
+
+
+  record IsSuccessorSetIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isSuccessorSetMonomorphism : IsSuccessorSetMonomorphism ⟦_⟧
+      surjective                 : Surjective _≈₁_ _≈₂_ ⟦_⟧
+
+    open IsSuccessorSetMonomorphism isSuccessorSetMonomorphism public
+
+    isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
+    isRelIsomorphism = record
+      { isMonomorphism = isRelMonomorphism
+      ; surjective     = surjective
+      }
+
+
 ------------------------------------------------------------------------
 -- Morphisms over magma-like structures
 ------------------------------------------------------------------------

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 IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set (a ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    suc#-cong     : Congruent₁ suc#
+
+  open IsEquivalence isEquivalence public
+
+  setoid : Setoid a ℓ
+  setoid = record { isEquivalence = isEquivalence }
+
 ------------------------------------------------------------------------
 -- Structures with 1 binary operation
 ------------------------------------------------------------------------