饂飩はモノイド(https://twitter.com/tanakh/status/325586411191427073)について

饂飩.agda

-- 饂飩はモノイドについて
-- https://twitter.com/tanakh/status/325586411191427073
--
module 饂飩 where

open import Data.List as List using (List; []; _∷_; _++_)
open import Algebra

data 基本味 : Set where
  たぬき : 基本味
  きつね : 基本味
  山菜   : 基本味
  カレー : 基本味
  ちから : 基本味
  -- まぁ，他にもあるだろうけどこのくらいで

record 饂飩 : Set where
  constructor _饂飩
  field
    味 : List 基本味

素饂飩 : 饂飩
素饂飩 = record { 味 = [] }

たぬき饂飩 : 饂飩
たぬき饂飩 = record { 味 = たぬき ∷ [] }

_+_ : 饂飩 → 饂飩 → 饂飩
(味₁ 饂飩) + (味₂ 饂飩) = record { 味 = 味₁ ++ 味₂ }

monoid : ∀ {ℓ} → Set ℓ → Monoid _ _
monoid A = record
  { Carrier  = 饂飩
  ; _≈_      = _≡_
  ; _∙_      = _+_
  ; ε        = 素饂飩
  ; isMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = assoc
      ; ∙-cong        = cong₂ _+_
      }
    ; identity = ((λ _ → refl) , identity)
    }
  }
  where
  open import Data.Product
  import Relation.Binary.PropositionalEquality as PropEq
  import Algebra.FunctionProperties as FunProp
  open PropEq using (_≡_; refl; cong₂)
  open FunProp _≡_
  module LM {a} (A : Set a) = Monoid (List.monoid A)

  identity : RightIdentity 素饂飩 _+_
  identity (味 饂飩)
    rewrite proj₂ (LM.identity 基本味) 味
          = refl

  assoc : Associative _+_
  assoc (味₁ 饂飩) (味₂ 饂飩) (味₃ 饂飩)
    rewrite LM.assoc 基本味 味₁ 味₂ 味₃
          = refl