Skip to content

Classical.Small.Structures.Monoid

Level-fixed Monoid

This is the Classical.Small.Structures.Monoid module of the Agda Universal Algebra Library.

Specializes Classical.Structures.Monoid to the common case where the universe level of both the carrier and the equivalence is 0โ„“ (i.e., Set-valued carriers with propositional or set-truncated equivalence), mirroring the analogous veneers for Magma, Semigroup, etc.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Small.Structures.Monoid where

open import Agda.Primitive                         using () renaming ( Set to Type )
open import Level                                  using ( 0โ„“ ; suc )
open import Relation.Binary.PropositionalEquality  using ( _โ‰ก_ )

import Classical.Structures.Monoid as Polymorphic

Monoid : Type (suc 0โ„“)
Monoid = Polymorphic.Monoid 0โ„“ 0โ„“

eqsToMonoid : (A : Type 0โ„“) (_ยท_ : A โ†’ A โ†’ A) (e : A)
  โ†’ (โˆ€ a b c โ†’ (a ยท b) ยท c โ‰ก a ยท (b ยท c))
  โ†’ (โˆ€ a โ†’ e ยท a โ‰ก a) โ†’ (โˆ€ a โ†’ a ยท e โ‰ก a)
  โ†’ Monoid
eqsToMonoid A = Polymorphic.eqsToMonoid {A = A}