------------------------------------------------------------------------ -- The Agda standard library -- -- Some theory for Semigroup ------------------------------------------------------------------------ {-# OPTIONS --without-K --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)