代表自由团体的好方法是什么？

很容易表示自由岩浆（二叉叶树）、自由半群（非空列表）和自由幺半群（列表），并且不难证明它们实际上就是它们所声称的那样。但自由团体似乎要棘手得多。似乎至少有两种方法可以使用通常的方法List (Either a)表示：

1. 将要求编码为类型，如果您有Left a :: Right b :: ... then Not (a = b)反之亦然。建造这些似乎有点困难。
2. 处理允许任意插入/删除的等价关系Left a :: Right a :: ...成对（反之亦然）。表达这种关系似乎极其复杂。

还有其他人有更好的主意吗？

Edit

我刚刚意识到唯一答案使用的选项（1）在最一般的设置中根本无法工作。特别是，如果不强加可判定的相等性，就不可能定义组运算！

Edit 2

我应该先想到谷歌这个。看起来像约阿希姆·布莱特纳在阿格达做的 https://www.joachim-breitner.de/blog/552-Free_Groups_in_Agda几年前，从他的介绍性描述来看，他似乎从选项 1 开始，但最终选择了选项 2。我想我会自己尝试一下，如果我陷入困境，我会看看他的代码。

作为第一个近似值，我将此数据类型定义为

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)

但这种双重前置对我来说看起来并不乐观。