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

Question

很容易表示自由岩浆(二元叶子树),自由半群(非空列表)和自由幺半群(列表),并且不难证明它们实际上是他们声称的那样.但自由团体似乎更棘手.似乎至少有两种使用常规List (Either a)表示的方法:

1. 在类型中编码要求,如果你有,Left a :: Right b :: ...那么Not (a = b)相反.构建这些似乎有点困难.
2. 研究等价关系,允许任意插入/删除Left a :: Right a :: ...对(以及相反的方式).表达这种关系似乎非常复杂.

其他人有更好的主意吗？

编辑

我刚刚意识到唯一的答案所使用的选项(1)根本无法在最常规的设置中工作.特别是,如果不实施可判定的平等,就无法定义组操作!

编辑2

我应该首先想到Google.看起来Joachim Breitner 几年前在Agda做过,从他的介绍性描述来看,看起来他从选项1开始,但最终选择了选项2.我想我会自己尝试,如果我太卡住了我会看看他的代码.

Answer 1

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

\n\n

open import Relation.Binary.PropositionalEquality\nopen import Data.Sum\nopen import Data.List\n\ninfixr 5 _\xe2\x88\xb7\xe1\xb6\xa0_\n\ninvert : \xe2\x88\x80 {\xce\xb1} {A : Set \xce\xb1} -> A \xe2\x8a\x8e A -> A \xe2\x8a\x8e A\ninvert (inj\xe2\x82\x81 x) = inj\xe2\x82\x82 x\ninvert (inj\xe2\x82\x82 x) = inj\xe2\x82\x81 x\n\ndata Consable {\xce\xb1} {A : Set \xce\xb1} (x : A \xe2\x8a\x8e A) : List (A \xe2\x8a\x8e A) -> Set \xce\xb1 where\n  nil  : Consable x []\n  cons : \xe2\x88\x80 {y xs} -> x \xe2\x89\xa2 invert y -> Consable x (y \xe2\x88\xb7 xs)\n\ndata FreeGroup {\xce\xb1} {A : Set \xce\xb1} : List (A \xe2\x8a\x8e A) -> Set \xce\xb1 where\n  []\xe1\xb6\xa0  : FreeGroup []\n  _\xe2\x88\xb7\xe1\xb6\xa0_ : \xe2\x88\x80 {x xs} -> Consable x xs -> FreeGroup xs -> FreeGroup (x \xe2\x88\xb7 xs)\n

\n\n

另一种变体是

\n\n

data FreeGroup {\xce\xb1} {A : Set \xce\xb1} : List (A \xe2\x8a\x8e A) -> Set \xce\xb1 where\n  Nil   : FreeGroup []\n  Cons1 : \xe2\x88\x80 x -> FreeGroup (x \xe2\x88\xb7 [])\n  Cons2 : \xe2\x88\x80 {x y xs} -> x \xe2\x89\xa2 invert y -> FreeGroup (y \xe2\x88\xb7 xs) -> FreeGroup (x \xe2\x88\xb7 y \xe2\x88\xb7 xs)\n

\n\n

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

\n