{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles using (Monoid)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
open Monoid M
renaming
( _∙_ to _+_
; ∙-cong to +-cong
; ∙-congʳ to +-congʳ
; ∙-congˡ to +-congˡ
; identityˡ to +-identityˡ
; identityʳ to +-identityʳ
; assoc to +-assoc
; ε to 0#
)
open import Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Definitions _≈_
open import Algebra.Definitions.RawMonoid rawMonoid public
using (_×_)
×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
×-congʳ 0 x≈x′ = refl
×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′)
×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×-cong {n} ≡.refl x≈x′ = ×-congʳ n x≈x′
×-congˡ : ∀ {x} → (_× x) Preserves _≡_ ⟶ _≈_
×-congˡ m≡n = ×-cong m≡n refl
×-homo-0 : ∀ x → 0 × x ≈ 0#
×-homo-0 x = refl
×-homo-1 : ∀ x → 1 × x ≈ x
×-homo-1 = +-identityʳ
×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x
×-homo-+ x 0 n = sym (+-identityˡ (n × x))
×-homo-+ x (suc m) n = begin
x + (m ℕ.+ n) × x ≈⟨ +-cong refl (×-homo-+ x m n) ⟩
x + (m × x + n × x) ≈⟨ sym (+-assoc x (m × x) (n × x)) ⟩
x + m × x + n × x ∎
×-idem : ∀ {c} → _+_ IdempotentOn c →
∀ n → .{{_ : NonZero n}} → n × c ≈ c
×-idem {c} idem (suc zero) = +-identityʳ c
×-idem {c} idem (suc n@(suc _)) = begin
c + (n × c) ≈⟨ +-congˡ (×-idem idem n ) ⟩
c + c ≈⟨ idem ⟩
c ∎
×-assocˡ : ∀ x m n → m × (n × x) ≈ (m ℕ.* n) × x
×-assocˡ x zero n = refl
×-assocˡ x (suc m) n = begin
n × x + m × n × x ≈⟨ +-congˡ (×-assocˡ x m n) ⟩
n × x + (m ℕ.* n) × x ≈⟨ ×-homo-+ x n (m ℕ.* n) ⟨
(suc m ℕ.* n) × x ∎