    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Multiplication over a monoid (i.e. repeated addition) optimised for
    -- type checking.
    ------------------------------------------------------------------------

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

    open import Algebra.Bundles using (Monoid)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
    open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

    module Algebra.Properties.Monoid.Mult.TCOptimised
      {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 Algebra.Properties.Monoid.Mult M as U
      using () renaming (_×_ to _×ᵤ_)

    open import Relation.Binary.Reasoning.Setoid setoid

    ------------------------------------------------------------------------
    -- Definition

    open import Algebra.Definitions.RawMonoid rawMonoid public
      using () renaming (_×′_ to _×_)

    ------------------------------------------------------------------------
    -- Properties

    1+× : ∀ n x → suc n × x ≈ x + n × x
    1+× 0               x = sym (+-identityʳ x)
    1+× 1               x = refl
    1+× (suc n@(suc _)) x = begin
      (suc n × x) + x ≈⟨ +-congʳ (1+× n x) ⟩
      (x + n × x) + x ≈⟨ +-assoc x (n × x) x ⟩
      x + (n × x + x) ∎

    -- The unoptimised (_×ᵤ_) and optimised (_×_) versions of multiplication
    -- are extensionally equal (up to the setoid equivalence).

    ×ᵤ≈× : ∀ n x → n ×ᵤ x ≈ n × x
    ×ᵤ≈× 0       x = refl
    ×ᵤ≈× (suc n) x = begin
      x + n ×ᵤ x  ≈⟨ +-congˡ (×ᵤ≈× n x) ⟩
      x + n ×  x  ≈⟨ 1+× n x ⟨
      suc n ×  x  ∎

    -- _×_ is homomorphic with respect to _ℕ.+_/_+_.

    ×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c
    ×-homo-+ c m n = begin
      (m ℕ.+ n) ×  c   ≈⟨ ×ᵤ≈× (m ℕ.+ n) c ⟨
      (m ℕ.+ n) ×ᵤ c   ≈⟨ U.×-homo-+ c m n ⟩
      m ×ᵤ c + n ×ᵤ c  ≈⟨ +-cong (×ᵤ≈× m c) (×ᵤ≈× n c) ⟩
      m ×  c + n ×  c  ∎

    -- _×_ preserves equality.

    ×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
    ×-congʳ 0               x≈y = refl
    ×-congʳ 1               x≈y = x≈y
    ×-congʳ (suc n@(suc _)) x≈y = +-cong (×-congʳ n x≈y) x≈y

    ×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
    ×-cong {n} ≡.refl x≈y = ×-congʳ n x≈y

    ×-assocˡ : ∀ x m n → m × (n × x) ≈ (m ℕ.* n) × x
    ×-assocˡ x m n = begin
      m ×  (n ×  x)  ≈⟨ ×-congʳ m (×ᵤ≈× n x) ⟨
      m ×  (n ×ᵤ x)  ≈⟨ ×ᵤ≈× m (n ×ᵤ x) ⟨
      m ×ᵤ (n ×ᵤ x)  ≈⟨  U.×-assocˡ x m n ⟩
      (m ℕ.* n) ×ᵤ x ≈⟨  ×ᵤ≈× (m ℕ.* n) x ⟩
      (m ℕ.* n) ×  x ∎