------------------------------------------------------------------------
-- The Agda standard library
--
-- 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.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --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 }

rawNearSemiring : RawNearSemiring c β„“
rawNearSemiring = 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 }

nearSemiring : NearSemiring c β„“
nearSemiring = record { 𝕆ne }

semiring : Semiring c β„“
semiring = record { 𝕆ne }

ring : Ring c β„“
ring = record { 𝕆ne }