It's easy to represent free magmas (binary leaf trees), free semigroups (non-empty lists), and free monoids (lists), and not hard to prove that they actually are what they claim to be. But free groups seem a lot trickier. There seem to be at least two approaches to using the usual List (Either a)
representation:
Left a :: Right b :: ...
then Not (a = b)
and the other way around. It seems likely to be a bit tough to build these.Left a :: Right a :: ...
pairs (and the other way around). Expressing this relation seems horrifyingly complicated.Anyone else have a better idea?
I just realized that option (1), which the sole answer uses, simply cannot work in the most general setting. In particular, it becomes impossible to define the group operation without imposing decidable equality!
I should've thought to Google this first. It looks like Joachim Breitner did it in Agda a few years ago, and from his introductory description, it looks like he started with option 1, but ultimately chose option 2. I guess I'll attempt it myself, and if I get too stuck I'll look at his code.
As a first approximation I would define this data type as
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)
One another variant is
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)
but this double prepending doesn't look promising to me.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With