[fixes #2273] Add SuccessorSet and associated boilerplate

CHANGELOG.md

@@ -51,11 +51,22 @@ 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.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts.
 
@@ -95,6 +106,14 @@ 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.Monoid.Mult`:
   ```agda
   ×-homo-0 : ∀ x → 0 × x ≈ 0#
@@ -108,6 +127,11 @@ Additions to existing modules
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
+* In `Algebra.Structures`
+  ```agda
+  record IsSuccessorSet (+1# : Op₁ A) (0# : A) : Set _
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

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 ( 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  8 _+1#
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _+1#             : Op₁ Carrier
+    0#               : Carrier
+    isSuccessorSet   : IsSuccessorSet _≈_ _+1# 0#
+
+  open IsSuccessorSet isSuccessorSet public
+
+  rawSuccessorSet : RawSuccessorSet _ _
+  rawSuccessorSet = record { _≈_ = _≈_; _+1# = _+1#; 0# = 0# }
+
+  open RawSuccessorSet rawSuccessorSet public
+
 ------------------------------------------------------------------------
 -- Bundles with 1 binary operation
 ------------------------------------------------------------------------

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 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
+
 ------------------------------------------------------------------------
 -- 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 _≈₁_; _+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 IsSuccessorSetHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
+      +1#-homo          : Homomorphic₁ ⟦_⟧ _+1#₁ _+1#₂
+      0#-homo           : Homomorphic₀ ⟦_⟧ 0#₁ 0#₂
+
+  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 (+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
 ------------------------------------------------------------------------