initial+terminal algebras

CHANGELOG.md

@@ -605,6 +605,8 @@ Non-backwards compatible changes
 
 * New modules:
   ```
+  Algebra.Construct.Initial
+  Algebra.Construct.Terminal
   Data.List.Effectful.Transformer
   Data.List.NonEmpty.Effectful.Transformer
   Data.Maybe.Effectful.Transformer
@@ -870,6 +872,14 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Construct.Zero`:
+  ```agda
+  rawMagma   ↦  Algebra.Construct.Terminal.rawMagma
+  magma      ↦  Algebra.Construct.Terminal.magma
+  semigroup  ↦  Algebra.Construct.Terminal.semigroup
+  band       ↦  Algebra.Construct.Terminal.band
+  ```
+
 * In `Codata.Guarded.Stream.Properties`:
   ```agda
   map-identity  ↦  map-id

src/Algebra/Construct/Initial.agda

@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- 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.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Initial {c ℓ : Level} where
+
+open import Algebra.Bundles
+  using (Magma; Semigroup; Band)
+open import Algebra.Bundles.Raw
+  using (RawMagma)
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Congruent₂)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
+open import Data.Empty.Polymorphic
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+
+------------------------------------------------------------------------
+-- Re-export those algebras which are also terminal
+
+open import Algebra.Construct.Terminal {c} {ℓ} public
+  hiding (rawMagma; magma; semigroup; band)
+
+------------------------------------------------------------------------
+-- Gather all the functionality in one place
+
+module ℤero where
+
+  infixl 7 _∙_
+  infix  4 _≈_
+
+  Carrier : Set c
+  Carrier = ⊥
+
+  _≈_     : Rel Carrier ℓ
+  _≈_ ()
+
+  _∙_     : Op₂ Carrier
+  _∙_ ()
+
+  refl : Reflexive _≈_
+  refl {x = ()}
+
+  sym : Symmetric _≈_
+  sym {x = ()}
+
+  trans : Transitive _≈_
+  trans {i = ()}
+
+  ∙-cong : Congruent₂ _≈_ _∙_
+  ∙-cong {x = ()}
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { ℤero }
+
+------------------------------------------------------------------------
+-- Structures
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record { ℤero }
+
+isMagma : IsMagma _≈_ _∙_
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
+isSemigroup : IsSemigroup _≈_ _∙_
+isSemigroup = record { isMagma = isMagma ; assoc = λ () }
+
+isBand : IsBand _≈_ _∙_
+isBand = record { isSemigroup = isSemigroup ; idem = λ () }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { isMagma = isMagma }
+
+semigroup : Semigroup c ℓ
+semigroup = record { isSemigroup = isSemigroup }
+
+band : Band c ℓ
+band = record { isBand = isBand }
+

src/Algebra/Construct/Terminal.agda

@@ -0,0 +1,86 @@
+------------------------------------------------------------------------
+-- 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).
+--
+-- From monoids up, these are zero-objects – i.e, both the initial
+-- and the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Terminal {c ℓ : Level} where
+
+open import Algebra.Bundles
+open import Data.Unit.Polymorphic
+open import Relation.Binary.Core using (Rel)
+
+------------------------------------------------------------------------
+-- Gather all the functionality in one place
+
+module 𝕆ne where
+
+  infix  4 _≈_
+  Carrier : Set c
+  Carrier = ⊤
+
+  _≈_     : Rel Carrier ℓ
+  _ ≈ _ = ⊤
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { 𝕆ne }
+
+rawMonoid : RawMonoid c ℓ
+rawMonoid = record { 𝕆ne }
+
+rawGroup : RawGroup c ℓ
+rawGroup = record { 𝕆ne }
+
+rawSemiring : RawSemiring c ℓ
+rawSemiring = record { 𝕆ne }
+
+rawRing : RawRing c ℓ
+rawRing = record { 𝕆ne }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { 𝕆ne }
+
+semigroup : Semigroup c ℓ
+semigroup = record { 𝕆ne }
+
+band : Band c ℓ
+band = record { 𝕆ne }
+
+commutativeSemigroup : CommutativeSemigroup c ℓ
+commutativeSemigroup = record { 𝕆ne }
+
+monoid : Monoid c ℓ
+monoid = record { 𝕆ne }
+
+commutativeMonoid : CommutativeMonoid c ℓ
+commutativeMonoid = record { 𝕆ne }
+
+idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
+idempotentCommutativeMonoid = record { 𝕆ne }
+
+group : Group c ℓ
+group = record { 𝕆ne }
+
+abelianGroup : AbelianGroup c ℓ
+abelianGroup = record { 𝕆ne }
+
+semiring : Semiring c ℓ
+semiring = record { 𝕆ne }
+
+ring : Ring c ℓ
+ring = record { 𝕆ne }
+

src/Algebra/Construct/Zero.agda

@@ -2,13 +2,15 @@
 -- The Agda standard library
 --
 -- Instances of algebraic structures where the carrier is ⊤.
--- In mathematics, this is usually called 0.
+-- In mathematics, this is usually called 0 (1 in the case of Group).
 --
 -- From monoids up, these are are zero-objects – i.e, both the initial
 -- and the terminal object in the relevant category.
--- For structures without an identity element, we can't necessarily
--- produce a homomorphism out of 0, because there is an instance of such
--- a structure with an empty Carrier.
+--
+-- For structures without an identity element, the terminal algebra is
+-- *not*  initial, because there is an instance of such a structure
+-- with an empty Carrier. Accordingly, such definitions are now deprecated
+-- in favour of those defined in `Algebra.Construct.Terminal`.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -17,47 +19,51 @@ open import Level using (Level)
 
 module Algebra.Construct.Zero {c ℓ : Level} where
 
+open import Algebra.Bundles.Raw
+  using (RawMagma)
 open import Algebra.Bundles
-open import Data.Unit.Polymorphic
+  using (Magma; Semigroup; Band)
 
 ------------------------------------------------------------------------
--- Raw bundles
+-- Re-export those algebras which are both initial and terminal
 
-rawMagma : RawMagma c ℓ
-rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+open import Algebra.Construct.Terminal public
+  hiding (rawMagma; magma; semigroup; band)
 
-rawMonoid : RawMonoid c ℓ
-rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new definitions re-exported from
+-- `Algebra.Construct.Terminal` as continuing support for the below is
+-- not guaranteed.
 
-rawGroup : RawGroup c ℓ
-rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+-- Version 2.0
 
-------------------------------------------------------------------------
--- Bundles
+rawMagma : RawMagma c ℓ
+rawMagma = Algebra.Construct.Terminal.rawMagma
+
+{-# WARNING_ON_USAGE rawMagma
+"Warning: rawMagma was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.rawMagma instead."
+#-}
 
 magma : Magma c ℓ
-magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+magma = Algebra.Construct.Terminal.magma
+{-# WARNING_ON_USAGE magma
+"Warning: magma was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.magma instead."
+#-}
 
 semigroup : Semigroup c ℓ
-semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+semigroup = Algebra.Construct.Terminal.semigroup
+{-# WARNING_ON_USAGE semigroup
+"Warning: semigroup was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.semigroup instead."
+#-}
 
 band : Band c ℓ
-band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-commutativeSemigroup : CommutativeSemigroup c ℓ
-commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-monoid : Monoid c ℓ
-monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-commutativeMonoid : CommutativeMonoid c ℓ
-commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ
-idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-group : Group c ℓ
-group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
-
-abelianGroup : AbelianGroup c ℓ
-abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
+band = Algebra.Construct.Terminal.band
+{-# WARNING_ON_USAGE semigroup
+"Warning: semigroup was deprecated in v2.0.
+Please use Algebra.Construct.Terminal.semigroup instead."
+#-}