------------------------------------------------------------------------ -- 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 open import Algebra.Definitions _≈_ open import Data.Product.Base using (_,_) 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) alternativeˡ : LeftAlternative _∙_ alternativeˡ x y = assoc x x y alternativeʳ : RightAlternative _∙_ alternativeʳ x y = sym (assoc x y y) alternative : Alternative _∙_ alternative = alternativeˡ , alternativeʳ flexible : Flexible _∙_ flexible x y = assoc x y x