From cc6a8e7c1f1d8b7b170dcfa12d1acb9bb2edd28c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 Jul 2024 10:43:10 +0100 Subject: [PATCH] fixes #2408 --- .../IdempotentCommutativeMonoid.agda | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 src/Algebra/Properties/IdempotentCommutativeMonoid.agda diff --git a/src/Algebra/Properties/IdempotentCommutativeMonoid.agda b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda new file mode 100644 index 0000000000..5c0a28252a --- /dev/null +++ b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda @@ -0,0 +1,38 @@ +------------------------------------------------------------------------ +-- 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ˡ