Add unique morphisms from/to Initial and Terminal algebras (#2296)

* added unique morphisms

* refactored for uniformity's sake

* exploit the uniformity

* add missing instances

* finish up, for now

* `CHANGELOG`

* `CHANGELOG`

* `TheMorphism`

* comment

* comment

* comment

* `The` to `Unique`

* lifted out istantiated `import`

* blank line

* note on instantiated `import`s

* parametrise on the `Raw` bundle

* parametrise on the `Raw` bundle

* Rerranged to get rid of lots of boilerplate

---------

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

CHANGELOG.md

@@ -50,6 +50,12 @@ New modules
 -----------
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
+* The unique morphism from the initial, resp. terminal, algebra:
+  ```agda
+  Algebra.Morphism.Construct.Initial
+  Algebra.Morphism.Construct.Terminal
+  ```
+
 * Nagata's construction of the "idealization of a module":
   ```agda
   Algebra.Module.Construct.Idealization
@@ -117,6 +123,12 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Construct.Terminal`:
+  ```agda
+  rawNearSemiring : RawNearSemiring c ℓ
+  nearSemiring    : NearSemiring c ℓ
+  ```
+
 * In `Algebra.Properties.Monoid.Mult`:
   ```agda
   ×-homo-0 : ∀ x → 0 × x ≈ 0#

doc/style-guide.md

@@ -131,6 +131,10 @@ automate most of this.
   open SetoidEquality S
   ```
 
+* If importing a parametrised module, qualified or otherwise, with its
+  parameters instantiated, then such 'instantiated imports' should be placed
+  *after* the main block of `import`s, and *before* any `variable` declarations.
+
 * Naming conventions for qualified `import`s: if importing a module under
   a root of the form `Data.X` (e.g. the `Base` module for basic operations,
   or `Properties` for lemmas about them etc.) then conventionally, the

src/Algebra/Construct/Initial.agda

@@ -4,8 +4,8 @@
 -- Instances of algebraic structures where the carrier is ⊥.
 -- In mathematics, this is usually called 0.
 --
--- From monoids up, these are zero-objects – i.e, the initial
--- object is the terminal object in the relevant category.
+-- From monoids up, these are zero-objects – i.e, the terminal
+-- object is *also* the initial object in the relevant category.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

src/Algebra/Construct/Terminal.agda

@@ -1,8 +1,8 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Instances of algebraic structures where the carrier is ⊤.
--- In mathematics, this is usually called 0 (1 in the case of Group).
+-- Instances of algebraic structures where the carrier is ⊤. In
+-- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
 --
 -- From monoids up, these are zero-objects – i.e, both the initial
 -- and the terminal object in the relevant category.
@@ -27,7 +27,7 @@ module 𝕆ne where
   Carrier : Set c
   Carrier = ⊤
 
-  _≈_     : Rel Carrier ℓ
+  _≈_   : Rel Carrier ℓ
   _ ≈ _ = ⊤
 
 ------------------------------------------------------------------------
@@ -42,6 +42,9 @@ rawMonoid = record { 𝕆ne }
 rawGroup : RawGroup c ℓ
 rawGroup = record { 𝕆ne }
 
+rawNearSemiring : RawNearSemiring c ℓ
+rawNearSemiring = record { 𝕆ne }
+
 rawSemiring : RawSemiring c ℓ
 rawSemiring = record { 𝕆ne }
 
@@ -78,6 +81,9 @@ group = record { 𝕆ne }
 abelianGroup : AbelianGroup c ℓ
 abelianGroup = record { 𝕆ne }
 
+nearSemiring : NearSemiring c ℓ
+nearSemiring = record { 𝕆ne }
+
 semiring : Semiring c ℓ
 semiring = record { 𝕆ne }
 

src/Algebra/Construct/Zero.agda

@@ -1,8 +1,8 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Instances of algebraic structures where the carrier is ⊤.
--- In mathematics, this is usually called 0 (1 in the case of Group).
+-- Instances of algebraic structures where the carrier is ⊤. In
+-- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
 --
 -- From monoids up, these are are zero-objects – i.e, both the initial
 -- and the terminal object in the relevant category.

src/Algebra/Morphism/Construct/Initial.agda

@@ -0,0 +1,62 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The unique morphism from the initial object,
+-- for each of the relevant categories. Since
+-- `Semigroup` and `Band` are simply `Magma`s
+-- satisfying additional properties, it suffices to
+-- define the morphism on the underlying `RawMagma`.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Morphism.Construct.Initial {c ℓ : Level} where
+
+open import Algebra.Bundles.Raw using (RawMagma)
+open import Algebra.Morphism.Structures
+open import Function.Definitions using (Injective)
+import Relation.Binary.Morphism.Definitions as Rel
+open import Relation.Binary.Morphism.Structures
+open import Relation.Binary.Core using (Rel)
+
+open import Algebra.Construct.Initial {c} {ℓ}
+
+private
+  variable
+    a m ℓm : Level
+    A : Set a
+    ≈ : Rel A ℓm
+
+------------------------------------------------------------------------
+-- The unique morphism
+
+zero : ℤero.Carrier → A
+zero ()
+
+------------------------------------------------------------------------
+-- Basic properties
+
+cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero
+cong _ {x = ()} 
+
+injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero
+injective _ {x = ()}
+
+------------------------------------------------------------------------
+-- Morphism structures
+
+isMagmaHomomorphism : (M : RawMagma m ℓm) →
+                      IsMagmaHomomorphism rawMagma M zero
+isMagmaHomomorphism M = record
+  { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
+  ; homo = λ()
+  } 
+
+isMagmaMonomorphism : (M : RawMagma m ℓm) →
+                      IsMagmaMonomorphism rawMagma M zero
+isMagmaMonomorphism M = record
+  { isMagmaHomomorphism = isMagmaHomomorphism M
+  ; injective = injective (RawMagma._≈_ M)
+  }

src/Algebra/Morphism/Construct/Terminal.agda

@@ -0,0 +1,88 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The unique morphism to the terminal object,
+-- for each of the relevant categories. Since
+-- each terminal algebra builds on `Monoid`,
+-- possibly with additional (trivial) operations,
+-- satisfying additional properties, it suffices to
+-- define the morphism on the underlying `RawMonoid`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Morphism.Construct.Terminal {c ℓ : Level} where
+
+open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
+open import Algebra.Morphism.Structures
+
+open import Data.Product.Base using (_,_)
+open import Function.Definitions using (StrictlySurjective)
+import Relation.Binary.Morphism.Definitions as Rel
+open import Relation.Binary.Morphism.Structures
+
+open import Algebra.Construct.Terminal {c} {ℓ}
+
+private
+  variable
+    a ℓa : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- The unique morphism
+
+one : A → 𝕆ne.Carrier
+one _ = _
+
+------------------------------------------------------------------------
+-- Basic properties
+
+strictlySurjective : A → StrictlySurjective 𝕆ne._≈_ one
+strictlySurjective x _ = x , _
+
+------------------------------------------------------------------------
+-- Homomorphisms
+
+isMagmaHomomorphism : (M : RawMagma a ℓa) →
+                      IsMagmaHomomorphism M rawMagma one
+isMagmaHomomorphism M = record
+  { isRelHomomorphism = record { cong = _ }
+  ; homo = _
+  }
+
+isMonoidHomomorphism : (M : RawMonoid a ℓa) →
+                       IsMonoidHomomorphism M rawMonoid one
+isMonoidHomomorphism M = record
+  { isMagmaHomomorphism = isMagmaHomomorphism (RawMonoid.rawMagma M)
+  ; ε-homo = _
+  }
+
+isGroupHomomorphism : (G : RawGroup a ℓa) →
+                      IsGroupHomomorphism G rawGroup one
+isGroupHomomorphism G = record
+  { isMonoidHomomorphism = isMonoidHomomorphism (RawGroup.rawMonoid G)
+  ; ⁻¹-homo = λ _ → _
+  }
+
+isNearSemiringHomomorphism : (N : RawNearSemiring a ℓa) →
+                             IsNearSemiringHomomorphism N rawNearSemiring one
+isNearSemiringHomomorphism N = record
+  { +-isMonoidHomomorphism = isMonoidHomomorphism (RawNearSemiring.+-rawMonoid N)
+  ; *-homo = λ _ _ → _
+  }
+
+isSemiringHomomorphism : (S : RawSemiring a ℓa) →
+                         IsSemiringHomomorphism S rawSemiring one
+isSemiringHomomorphism S = record
+  { isNearSemiringHomomorphism = isNearSemiringHomomorphism (RawSemiring.rawNearSemiring S)
+  ; 1#-homo = _
+  }
+
+isRingHomomorphism : (R : RawRing a ℓa) → IsRingHomomorphism R rawRing one
+isRingHomomorphism R = record
+  { isSemiringHomomorphism = isSemiringHomomorphism (RawRing.rawSemiring R)
+  ; -‿homo = λ _ → _
+  }