[fix agda#2273] Add NNO-related modules

Author: jamesmckinna

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

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
 ------------------------------------------------------------------------

src/Algebra/Morphism/Structures.agda

@@ -6,21 +6,65 @@
 
 {-# 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 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
 ------------------------------------------------------------------------

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
 ------------------------------------------------------------------------