FreeMonoid.agda

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.List

private
  variable
    ℓ : Level
    A : Type ℓ

data Free (A : Type ℓ) : Type ℓ where
  ∅   : Free A
  ⟨_⟩ : A → Free A
  _⋆_ : Free A → Free A → Free A

  ⋆-idl   : ∀ x → ∅ ⋆ x ≡ x
  ⋆-idr   : ∀ x → x ⋆ ∅ ≡ x
  ⋆-assoc : ∀ x y z → (x ⋆ y) ⋆ z ≡ x ⋆ (y ⋆ z)

infixr 5 _⋆_

List→Free : List A → Free A
List→Free = foldr (λ x f → ⟨ x ⟩ ⋆ f) ∅

Free→List : Free A → List A
Free→List ∅ = []
Free→List ⟨ x ⟩ = [ x ]
Free→List (xs ⋆ ys) = Free→List xs ++ Free→List ys
Free→List (⋆-idl xs i) = Free→List xs
Free→List (⋆-idr xs i) = ++-unit-r (Free→List xs) i
Free→List (⋆-assoc xs ys zs i) = ++-assoc (Free→List xs) (Free→List ys) (Free→List zs) i

example-List→Free : List→Free (1 ∷ 2 ∷ []) ≡ ⟨ 1 ⟩ ⋆ ⟨ 2 ⟩ ⋆ ∅
example-List→Free = refl

example-Free→List : Free→List (∅ ⋆ ∅ ⋆ ⟨ 1 ⟩ ⋆ ∅ ⋆ ∅ ⋆ ⟨ 2 ⟩ ⋆ ∅) ≡ 1 ∷ 2 ∷ []
example-Free→List = refl

List→Free→List : (l : List A) → Free→List (List→Free l) ≡ l
List→Free→List [] = refl
List→Free→List (x ∷ xs) =
    Free→List (List→Free (x ∷ xs))
  ≡⟨ refl ⟩
    x ∷ Free→List (List→Free xs)
  ≡⟨ cong (x ∷_) (List→Free→List xs) ⟩
    x ∷ xs ∎

List→Free-++ : (xs ys : List A) → List→Free (xs ++ ys) ≡ List→Free xs ⋆ List→Free ys
List→Free-++ [] ys = sym (⋆-idl (List→Free ys))
List→Free-++ (x ∷ xs) ys =
    ⟨ x ⟩ ⋆ List→Free (xs ++ ys)
  ≡⟨ cong (⟨ x ⟩ ⋆_) (List→Free-++ xs ys) ⟩
    ⟨ x ⟩ ⋆ List→Free xs ⋆ List→Free ys
  ≡⟨ sym (⋆-assoc _ _ _) ⟩
    (⟨ x ⟩ ⋆ List→Free xs) ⋆ List→Free ys ∎

Free→List→Free : (f : Free A) → List→Free (Free→List f) ≡ f
Free→List→Free ∅ = refl
Free→List→Free ⟨ x ⟩ = ⋆-idr ⟨ x ⟩
Free→List→Free (xs ⋆ ys) =
    List→Free (Free→List xs ++ Free→List ys)
  ≡⟨ List→Free-++ (Free→List xs) (Free→List ys) ⟩
    List→Free (Free→List xs) ⋆ List→Free (Free→List ys)
  ≡⟨ cong₂ _⋆_ (Free→List→Free xs) (Free→List→Free ys) ⟩
    xs ⋆ ys ∎
Free→List→Free (⋆-idl x i) = {!  !}
Free→List→Free (⋆-idr x i) = {!  !}
Free→List→Free (⋆-assoc a b c i) = {!  !}

List≡Free : List A ≡ Free A
List≡Free = isoToPath (iso List→Free Free→List Free→List→Free List→Free→List)