thing.agda

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Nat using (Nat ; suc ; zero)
open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.Equality.Rewrite using ()

sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a)
sym refl = refl

trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
trans refl refl = refl

cong₂ : ∀ {A B C : Set} {a b : A} {c d : B} → (f : A → B → C) → (a ≡ b) → (c ≡ d) → (f a c ≡ f b d)
cong₂ f refl refl = refl

record Monoid : Set₁ where

  field A : Set
  field ε : A
  field _*_ : A → A → A

  field assoc : ∀ {a b c} → ((a * b) * c) ≡ (a * (b * c))
  field lunit  : ∀ {a} → (ε * a) ≡ a
  field runit  : ∀ {a} → (a * ε) ≡ a

  postulate _*′_ : A → A → A
  postulate *′-defn : ∀ {a b} → (a *′ b) ≡ (a * b)

  assoc′ : ∀ {a b c} → ((a *′ b) *′ c) ≡ (a *′ (b *′ c))
  assoc′ = trans (cong₂ _*′_ *′-defn refl) (trans *′-defn (trans assoc (trans (sym *′-defn) (cong₂ _*′_ refl (sym *′-defn)))))
  
  lunit′ : ∀ {a} → (ε *′ a) ≡ a
  lunit′ = trans *′-defn lunit
  
  runit′ : ∀ {a} → (a *′ ε) ≡ a
  runit′ = trans *′-defn runit

  {-# REWRITE assoc′ lunit′ runit′ #-}

-- Challenge: define append on lists indexed by an arbitrary monoid
record Test (M : Monoid) : Set where

  open Monoid M public
  
  data Thing : A → Set where

    nil : Thing ε
    cons : ∀ a → ∀ {b} → Thing b → Thing (a *′ b)

  append : ∀ {a b} → Thing a → Thing b → Thing (a *′ b) 
  append nil bs = bs
  append (cons a as) bs = cons a (append as bs)

Do I understand correctly that Thing a is the type of lists whose sum is a, i.e. decompositions of a as a formal sum? What is the purpose of _*′_?

The context is https://types.pl/@asaj/110844587990868150

and https://types.pl/@asaj/110839061117660866