------------------------------------------------------------------------
-- The Agda standard library
--
-- Some theory for Semigroup
------------------------------------------------------------------------

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

open import Algebra using (Semigroup)

module Algebra.Properties.Semigroup {a } (S : Semigroup a ) where

open Semigroup S

x∙yz≈xy∙z :  x y z  x  (y  z)  (x  y)  z
x∙yz≈xy∙z x y z = sym (assoc x y z)