    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Finite summations over a commutative monoid
    ------------------------------------------------------------------------

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

    open import Algebra.Bundles using (CommutativeMonoid)
    open import Data.Bool.Base using (Bool; true; false)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
    open import Data.Fin.Base using (Fin; zero; suc)
    open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
    open import Data.Fin.Patterns using (0F)
    open import Data.Vec.Functional using (Vector; rearrange; removeAt; tail; head)
    open import Function.Base using (_∘_)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    open import Relation.Nullary.Negation using (contradiction)

    module Algebra.Properties.CommutativeMonoid.Sum
      {a ℓ} (M : CommutativeMonoid a ℓ) where

    open CommutativeMonoid M
      renaming
      ( _∙_       to _+_
      ; ∙-cong    to +-cong
      ; ∙-congˡ   to +-congˡ
      ; identityˡ to +-identityˡ
      ; identityʳ to +-identityʳ
      ; assoc     to +-assoc
      ; ε         to 0#
      )

    open import Algebra.Definitions _≈_
    open import Algebra.Solver.CommutativeMonoid M
    open import Data.Vec.Functional.Relation.Binary.Equality.Setoid setoid
    open import Relation.Binary.Reasoning.Setoid setoid

    ------------------------------------------------------------------------
    -- Re-export summation over monoids

    open import Algebra.Properties.Monoid.Sum monoid public

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

    -- When summing over a function from a finite set, we can pull out any
    -- value and move it to the front.
    sum-remove : ∀ {n} {i : Fin (suc n)} t → sum t ≈ t i + sum (removeAt t i)
    sum-remove {_}     {zero}   xs = refl
    sum-remove {suc n} {suc i}  xs = begin
      t₀ + ∑t           ≈⟨ +-congˡ (sum-remove t) ⟩
      t₀ + (tᵢ + ∑t′)   ≈⟨ solve 3 (λ x y z → x ⊕ (y ⊕ z) ⊜ y ⊕ (x ⊕ z)) refl t₀ tᵢ ∑t′ ⟩
      tᵢ + (t₀ + ∑t′)   ∎
      where
      t = tail xs
      t₀ = head xs
      tᵢ = t i
      ∑t = sum t
      ∑t′ = sum (removeAt t i)

    -- The '∑' operator distributes over addition.
    ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
    ∑-distrib-+ {zero}  f g = sym (+-identityˡ _)
    ∑-distrib-+ {suc n} f g = begin
      f₀ + g₀ + ∑fg          ≈⟨ +-assoc _ _ _ ⟩
      f₀ + (g₀ + ∑fg)        ≈⟨ +-congˡ (+-congˡ (∑-distrib-+ (f ∘ suc) (g ∘ suc))) ⟩
      f₀ + (g₀ + (∑f + ∑g))  ≈⟨ solve 4 (λ a b c d → a ⊕ (c ⊕ (b ⊕ d)) ⊜ (a ⊕ b) ⊕ (c ⊕ d)) refl f₀ ∑f g₀ ∑g ⟩
      (f₀ + ∑f) + (g₀ + ∑g)  ∎
      where
      f₀ = f 0F
      g₀ = g 0F
      ∑f  = ∑[ i < n ] f (suc i)
      ∑g  = ∑[ i < n ] g (suc i)
      ∑fg = ∑[ i < n ] (f (suc i) + g (suc i))

    -- The '∑' operator commutes with itself.
    ∑-comm : ∀ {m n} (f : Fin m → Fin n → Carrier) →
             ∑[ i < m ] ∑[ j < n ] f i j ≈ ∑[ j < n ] ∑[ i < m ] f i j
    ∑-comm {zero}  {n} f = sym (sum-replicate-zero n)
    ∑-comm {suc m} {n} f = begin
      ∑[ j < n ] f zero j + ∑[ i < m ] ∑[ j < n ] f (suc i) j  ≈⟨ +-congˡ (∑-comm (f ∘ suc)) ⟩
      ∑[ j < n ] f zero j + ∑[ j < n ] ∑[ i < m ] f (suc i) j  ≈⟨ sym (∑-distrib-+ (f zero) _) ⟩
      ∑[ j < n ] (f zero j + ∑[ i < m ] f (suc i) j)           ∎

    -- Summation is insensitive to permutations of the input
    sum-permute : ∀ {m n} f (π : Permutation m n) → sum f ≈ sum (rearrange (π ⟨$⟩ʳ_) f)
    sum-permute {zero}  {zero}  f π = refl
    sum-permute {zero}  {suc n} f π = contradiction π (Perm.refute λ())
    sum-permute {suc m} {zero}  f π = contradiction π (Perm.refute λ())
    sum-permute {suc m} {suc n} f π = begin
      sum f                                    ≡⟨⟩
      f 0F  + sum f/0                          ≡⟨ ≡.cong (_+ sum f/0) (≡.cong f (Perm.inverseʳ π)) ⟨
      πf π₀ + sum f/0                          ≈⟨ +-congˡ (sum-permute f/0 (Perm.remove π₀ π)) ⟩
      πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0)  ≡⟨ ≡.cong (πf π₀ +_) (sum-cong-≗ (≡.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟨
      πf π₀ + sum (removeAt πf π₀)             ≈⟨ sym (sum-remove πf) ⟩
      sum πf                                   ∎
      where
      f/0 = removeAt f 0F
      π₀ = π ⟨$⟩ˡ 0F
      π/0 = Perm.remove π₀ π
      πf = rearrange (π ⟨$⟩ʳ_) f

    ∑-permute : ∀ {m n} (f : Vector Carrier n) (π : Permutation m n) →
                ∑[ i < n ] f i ≈ ∑[ i < m ] f (π ⟨$⟩ʳ i)
    ∑-permute f π = sum-permute f π