[Agda] Associativity for free!

[James Chapman]

It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.

First some machinery:

{-# OPTIONS --type-in-type #-}

module Cayley where

data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
  refl : a ≡ a

sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
sym refl = refl

ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
ir {p = refl} {q = refl} = refl

fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
' → a' ≡ a''' → p ≡ q
fixtypes refl refl = ir

cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
cong f refl = refl

id : {X : Set} → X → X
id = λ x → x

_◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
f ◦ g = λ x → f (g x)

Given any monoid (M) where the monoid laws hold propositionally:

record Monoid : Set1 where
  field set : Set
        ε   : set
        _•_ : set → set → set
        lid : ∀{m} → (ε • m) ≡ m
        rid : ∀{m} → (m • ε) ≡ m
        ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
open Monoid

We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where the monoidal structure given by identity and composition holds definitionally).
Morph : Monoid → Set
Morph M = set M → set M

MorphMon : Monoid → Monoid
MorphMon M = record {
  set = Morph M;
  ε   = id;
  _•_ = _◦_;
  lid = refl;
  rid = refl;
  ass = refl}

Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some m : M.

Here's a proof:

record Σ (A : Set)(P : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : P fst

open Σ

eqΣ : {I : Set}{i : I}{A A' : I -> Set}{a : A i}{i' : I}{a' : A' i'} ->
          i ≡ i' -> A ≡ A' -> a ≡ a' -> _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
eqΣ refl refl refl = refl

record Iso (X Y : Set) : Set where
  field fun   : X → Y
        inv   : Y → X
        left  : (fun ◦ inv) ≡ id {Y}
        right : (inv ◦ fun) ≡ id {X}

postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g

Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
Cayley M = record {
  fun   = λ m → (_•_ M m) , (m , refl);
  inv   = λ p → fst (snd p);
  left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡ (_•_ M x')) y) (fixtypes y refl));
  right = refl}

I wonder if we can use this trick for groups as well as monoids and get difference integers, difference 'nats (mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so we would need isos to have a monodical structure which holds definitionally. But the do if we mark the field left and right above as irrelevant:

_·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
f · g = record {
  fun   =  fun f ◦ fun g ;
  inv   = inv g ◦ inv f;
  left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
  right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}

idI : ∀{X} → Iso X X
idI {X} = record {
  fun   = id;
  inv   = id;
  left  = refl;
  right = refl}

ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
ridI f = refl

lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
lidI f = refl

assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
       (f · (g · h)) ≡ ((f · g) · h)
assI f g h = refl

So, it looks promising so far.

Regards,

James