Какой хороший способ представлять свободные группы?

Question

Легко представить свободные магмы (бинарные листовые деревья), свободные полугруппы (непустые списки) и свободные моноиды (списки), и нетрудно доказать, что они действительно являются теми, кем себя называют. Но свободные группы кажутся намного хитрее. Кажется, есть как минимум два подхода к использованию обычного List (Either a) представление:

1. Закодируйте в виде требование, что если у вас есть Left a :: Right b :: ... затем Not (a = b) и наоборот. Похоже, будет сложно создать их.
2. Работа над отношением эквивалентности, допускающим произвольную вставку / удаление Left a :: Right a :: ... пары (и наоборот). Выражение этой связи кажется ужасно сложным.

У кого-нибудь есть идея получше?

редактировать

Я только что понял, что опция (1), которую использует единственный ответ, просто не может работать в самых общих условиях. В частности, становится невозможным определить групповую операцию без наложения решительного равенства!

Редактировать 2

Я должен был подумать об этом Google в первую очередь. Похоже, что Иоахим Брейтнер сделал это в Агде несколько лет назад, и из его вступительного описания похоже, что он начал с варианта 1, но в конечном итоге выбрал вариант 2. Думаю, я попробую сам, и если я слишком застрял Я посмотрю на его код.

Answer 1

В первом приближении я бы определил этот тип данных как

open import Relation.Binary.PropositionalEquality
open import Data.Sum
open import Data.List

infixr 5 _∷ᶠ_

invert : ∀ {α} {A : Set α} -> A ⊎ A -> A ⊎ A
invert (inj₁ x) = inj₂ x
invert (inj₂ x) = inj₁ x

data Consable {α} {A : Set α} (x : A ⊎ A) : List (A ⊎ A) -> Set α where
  nil  : Consable x []
  cons : ∀ {y xs} -> x ≢ invert y -> Consable x (y ∷ xs)

data FreeGroup {α} {A : Set α} : List (A ⊎ A) -> Set α where
  []ᶠ  : FreeGroup []
  _∷ᶠ_ : ∀ {x xs} -> Consable x xs -> FreeGroup xs -> FreeGroup (x ∷ xs)

Еще один вариант

data FreeGroup {α} {A : Set α} : List (A ⊎ A) -> Set α where
  Nil   : FreeGroup []
  Cons1 : ∀ x -> FreeGroup (x ∷ [])
  Cons2 : ∀ {x y xs} -> x ≢ invert y -> FreeGroup (y ∷ xs) -> FreeGroup (x ∷ y ∷ xs)

но это двойное предположение не выглядит многообещающим для меня.