freemonoid.agda

{-# OPTIONS --cubical #-}

open import Cubical.Core.Prelude
open import Data.List hiding ([_])
open import Cubical.Foundations.Isomorphism

data FreeMonoid (A : Set) : Set where
  [_] : A -> FreeMonoid A
  _●_ : FreeMonoid A -> FreeMonoid A -> FreeMonoid A
  ε   : FreeMonoid A
  ∙ε  : ∀ x -> x ● ε ≡ x
  ε∙  : ∀ x -> ε ● x ≡ x
  assoc : ∀ x y z -> (x ● y) ● z ≡ x ● (y ● z)

variable
  A : Set

postulate FM-set : ∀ {A} -> isSet (FreeMonoid A)

++[] : (xs : List A) -> xs ++ [] ≡ xs
++[] [] = refl
++[] (x ∷ xs) = cong (x ∷_) (++[] xs)

++-assoc : (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-assoc xs ys zs = {!!} -- exercise

FM-to-List : FreeMonoid A -> List A
FM-to-List [ x ] = x ∷ []
FM-to-List (x ● y) = FM-to-List x ++ FM-to-List y
FM-to-List ε = []
FM-to-List (∙ε x i) = ++[] (FM-to-List x) i
FM-to-List (ε∙ x i) = FM-to-List x
FM-to-List (assoc x y z i) = {!!} -- by ++-assoc

List-to-FM : List A -> FreeMonoid A
List-to-FM [] = ε
List-to-FM (x ∷ xs) = [ x ] ● List-to-FM xs

lemma1 : (xs ys : List A) -> List-to-FM (xs ++ ys) ≡ List-to-FM xs ● List-to-FM ys
lemma1 [] ys = sym (ε∙ (List-to-FM ys))
lemma1 (x ∷ xs) ys = cong ([ x ] ●_) (lemma1 xs ys)
                   ∙ sym (assoc [ x ] (List-to-FM xs) (List-to-FM ys))

iso1 : (fm : FreeMonoid A) -> List-to-FM (FM-to-List fm) ≡ fm
iso1 [ x ] = ∙ε [ x ]
iso1 (fm ● fm') = lemma1 (FM-to-List fm) (FM-to-List fm')
                ∙ cong (List-to-FM (FM-to-List fm) ●_) (iso1 fm')
                ∙ cong (_● fm') (iso1 fm)
iso1 ε = refl
iso1 (∙ε fm i) = goal i
  where
    goal : PathP (λ i → List-to-FM (++[] (FM-to-List fm) i) ≡ ∙ε fm i)
                 _ (iso1 fm)
    goal = toPathP (FM-set _ _
            (transp (λ i₁ → List-to-FM (++[] (FM-to-List fm) i₁) ≡ ∙ε fm i₁) i0 _) _)
iso1 (ε∙ fm i) = {!!} -- exercise
iso1 (assoc fm fm₁ fm₂ i) = {!!} -- exercise

iso2 : (xs : List A) -> FM-to-List (List-to-FM xs) ≡ xs
iso2 [] = refl
iso2 (x ∷ xs) = cong (x ∷_) (iso2 xs)

samey : FreeMonoid A ≡ List A
samey = isoToPath (iso FM-to-List List-to-FM iso2 iso1)

open import Data.Nat

list-length : List A -> ℕ
list-length [] = 0
list-length (x ∷ xs) = 1 + list-length xs

-- fm-length comes for free
fm-length : FreeMonoid A -> ℕ
fm-length fm = list-length (subst (λ x → x) samey fm)