added unique morphisms

CHANGELOG.md

@@ -48,6 +48,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
+  ```
+
 Additions to existing modules
 -----------------------------
 

src/Algebra/Construct/Terminal.agda

@@ -27,7 +27,7 @@ module 𝕆ne where
   Carrier : Set c
   Carrier = ⊤
 
-  _≈_     : Rel Carrier ℓ
+  _≈_   : Rel Carrier ℓ
   _ ≈ _ = ⊤
 
 ------------------------------------------------------------------------

src/Algebra/Morphism/Construct/Initial.agda

@@ -0,0 +1,73 @@
+------------------------------------------------------------------------
+-- 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 using (Magma)
+open import Algebra.Bundles.Raw using (RawMagma)
+open import Algebra.Construct.Initial {c} {ℓ}
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Algebra.Morphism.Structures using (module MagmaMorphisms)
+open import Function.Definitions using (Injective)
+import Relation.Binary.Morphism.Definitions as Definitions
+open import Relation.Binary.Morphism.Structures
+
+private
+  variable
+    m ℓm : Level
+
+
+------------------------------------------------------------------------
+-- The underlying data of the morphism
+
+module ℤeroMorphism (M : RawMagma m ℓm) where
+
+  open RawMagma M
+  open MorphismDefinitions ℤero.Carrier Carrier _≈_
+
+  zero : ℤero.Carrier → Carrier
+  zero ()
+
+  cong : Definitions.Homomorphic₂ ℤero.Carrier Carrier ℤero._≈_ _≈_ zero
+  cong {x = ()}
+
+  isRelHomomorphism : IsRelHomomorphism ℤero._≈_ _≈_ zero
+  isRelHomomorphism = record { cong = cong }
+
+  homo : Homomorphic₂ zero ℤero._∙_ _∙_
+  homo ()
+
+  injective : Injective ℤero._≈_ _≈_ zero
+  injective {x = ()}
+
+------------------------------------------------------------------------
+-- Magma
+
+module _ (M : Magma m ℓm) where
+
+  private module M = Magma M
+  open MagmaMorphisms rawMagma M.rawMagma
+  open ℤeroMorphism M.rawMagma
+
+  isMagmaHomomorphism : IsMagmaHomomorphism zero
+  isMagmaHomomorphism = record
+    { isRelHomomorphism = isRelHomomorphism
+    ; homo = homo
+    }
+
+  isMagmaMonomorphism : IsMagmaMonomorphism zero
+  isMagmaMonomorphism = record
+    { isMagmaHomomorphism = isMagmaHomomorphism
+    ; injective = injective
+    }

src/Algebra/Morphism/Construct/Terminal.agda

@@ -0,0 +1,98 @@
+------------------------------------------------------------------------
+-- 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 using (Monoid; Group)
+open import Algebra.Bundles.Raw using (RawMonoid; RawGroup)
+open import Algebra.Construct.Terminal {c} {ℓ}
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Algebra.Morphism.Structures
+  using ( module MagmaMorphisms
+        ; module MonoidMorphisms
+        ; module GroupMorphisms
+        )
+open import Data.Product.Base using (_,_)
+open import Function.Definitions using (StrictlySurjective)
+import Relation.Binary.Morphism.Definitions as Definitions
+open import Relation.Binary.Morphism.Structures
+
+private
+  variable
+    a ℓa : Level
+
+
+------------------------------------------------------------------------
+-- The underlying data of the morphism
+
+module 𝕆neMorphism (M : RawMonoid a ℓa) where
+
+  open RawMonoid M
+  open MorphismDefinitions Carrier 𝕆ne.Carrier 𝕆ne._≈_
+
+  one : Carrier → 𝕆ne.Carrier
+  one _ = _
+
+  cong : Definitions.Homomorphic₂ Carrier 𝕆ne.Carrier _≈_ 𝕆ne._≈_ one
+  cong _ = _
+
+  isRelHomomorphism : IsRelHomomorphism _≈_ 𝕆ne._≈_ one
+  isRelHomomorphism = record { cong = cong }
+
+  homo : Homomorphic₂ one _∙_ _
+  homo _ = _
+
+  ε-homo : Homomorphic₀ one ε _
+  ε-homo = _
+
+  strictlySurjective : StrictlySurjective 𝕆ne._≈_ one
+  strictlySurjective _ = ε , _
+
+------------------------------------------------------------------------
+-- Monoid
+
+module _ (M : Monoid a ℓa) where
+
+  private module M = Monoid M
+  open MonoidMorphisms M.rawMonoid rawMonoid
+  open MagmaMorphisms M.rawMagma rawMagma
+  open 𝕆neMorphism M.rawMonoid
+
+  isMagmaHomomorphism : IsMagmaHomomorphism one
+  isMagmaHomomorphism = record
+    { isRelHomomorphism = isRelHomomorphism
+    ; homo = homo
+    }
+
+  isMonoidHomomorphism : IsMonoidHomomorphism one
+  isMonoidHomomorphism = record
+    { isMagmaHomomorphism = isMagmaHomomorphism
+    ; ε-homo = ε-homo
+    }
+
+------------------------------------------------------------------------
+-- Group
+
+module _ (G : Group a ℓa) where
+
+  private module G = Group G
+  open GroupMorphisms G.rawGroup rawGroup
+  open 𝕆neMorphism G.rawMonoid
+
+  isGroupHomomorphism : IsGroupHomomorphism one
+  isGroupHomomorphism = record
+    { isMonoidHomomorphism = isMonoidHomomorphism G.monoid
+    ; ⁻¹-homo = λ _ → _
+    }