------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra.Bundles using (IdempotentCommutativeMonoid)

module Algebra.Properties.IdempotentCommutativeMonoid
  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where

open IdempotentCommutativeMonoid M

open import Algebra.Consequences.Setoid setoid
  using (comm∧distrˡ⇒distrʳ; comm∧distrˡ⇒distr)
open import Algebra.Definitions _≈_
  using (_DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
  using (interchange)
open import Relation.Binary.Reasoning.Setoid setoid


------------------------------------------------------------------------
-- Distributivity

∙-distrˡ-∙ : _∙_ DistributesOverˡ _∙_
∙-distrˡ-∙ a b c = begin
    a ∙ (b ∙ c)        ≈⟨ ∙-congʳ (idem a) ⟨
    (a ∙ a) ∙ (b ∙ c)  ≈⟨ interchange _ _ _ _ ⟩
    (a ∙ b) ∙ (a ∙ c)  ∎

∙-distrʳ-∙ : _∙_ DistributesOverʳ _∙_
∙-distrʳ-∙ = comm∧distrˡ⇒distrʳ ∙-cong comm ∙-distrˡ-∙

∙-distr-∙ : _∙_ DistributesOver _∙_
∙-distr-∙ = comm∧distrˡ⇒distr ∙-cong comm ∙-distrˡ-∙