{-# OPTIONS --cubical --safe --exact-split #-}

module Cubical.Structures.Set.CMon.CList where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as 
import Cubical.Data.List as L

import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Set.CMon.Desc as M
import Cubical.Structures.Free as F
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity

infixr 20 _∷_

data CList {a} (A : Type a) : Type a where
  [] : CList A
  _∷_ : (a : A) -> (as : CList A) -> CList A
  comm : (a b : A)
      -> {as bs : CList A} (cs : CList A)
      -> (p : as  b  cs) (q : bs  a  cs)
      -> a  as  b  bs
  isSetCList : isSet (CList A)

pattern [_] a = a  []

module elimCListSet { p : Level} {A : Type } (P : CList A -> Type p)
                   ([]* : P [])
                   (_∷*_ : (x : A) {xs : CList A} -> P xs -> P (x  xs))
                   (comm* : (a b : A)
                            -> {as bs : CList A} {cs : CList A}
                            -> {as* : P as}
                            -> {bs* : P bs}
                            -> (cs* : P cs)
                            -> {p : as  b  cs} {q : bs  a  cs}
                            -> (bp : PathP  i -> P (p i)) as* (b ∷* cs*))
                            -> (bq : PathP  i -> P (q i)) bs* (a ∷* cs*))
                            -> PathP  i -> P (comm a b cs p q i)) (a ∷* as*) (b ∷* bs*)
                   )
                   (isSetCList* : {xs : CList A} -> isSet (P xs))
                   where
  f : (xs : CList A) -> P xs
  f [] = []*
  f (a  as) = a ∷* f as
  f (comm a b {as} {bs} cs p q i) =
    comm* a b (f cs) (cong f p) (cong f q) i
  f (isSetCList xs ys p q i j) =
    isOfHLevel→isOfHLevelDep 2  xs -> isSetCList* {xs = xs}) (f xs) (f ys) (cong f p) (cong f q) (isSetCList xs ys p q) i j

module elimCListProp { p : Level} {A : Type } (P : CList A -> Type p)
                   ([]* : P [])
                   (_∷*_ : (x : A) {xs : CList A} -> P xs -> P (x  xs))
                   (isSetCList* : {xs : CList A} -> isProp (P xs))
                   where
  f : (xs : CList A) -> P xs
  f = elimCListSet.f P []* _∷*_
     a b {as} {bs} {cs} {as*} {bs*} cs* bp bq -> toPathP (isSetCList* _ (b ∷* bs*)))
    (isProp→isSet isSetCList*)

private
  variable
     : Level
    A : Type 

_++_ : CList A -> CList A -> CList A
[] ++ bs = bs
(a  as) ++ bs = a  (as ++ bs)
comm a b cs p q i ++ bs = comm a b (cs ++ bs) (cong (_++ bs) p) (cong (_++ bs) q) i
isSetCList a b p q i j ++ bs = isSetCList (a ++ bs) (b ++ bs) (cong (_++ bs) p) (cong (_++ bs) q) i j

++-unitl : (as : CList A) -> [] ++ as  as
++-unitl as = refl

++-unitr : (as : CList A) -> as ++ []  as
++-unitr = elimCListProp.f _ refl  a p -> cong (a ∷_) p) (isSetCList _ _)

++-assocr : (as bs cs : CList A) -> (as ++ bs) ++ cs  as ++ (bs ++ cs)
++-assocr = elimCListProp.f _
   _ _ -> refl)
   x p bs cs -> cong (x ∷_) (p bs cs))
  (isPropΠ λ _ -> isPropΠ λ _ -> isSetCList _ _)

swap : (a b : A) (cs : CList A) -> a  b  cs  b  a  cs
swap a b cs = comm a b cs refl refl

++-∷ : (a : A) (as : CList A) -> a  as  as ++ [ a ]
++-∷ a = elimCListProp.f  as -> a  as  as ++ [ a ])
  refl
   b {as} p -> swap a b as  cong (b ∷_) p)
  (isSetCList _ _) 

++-comm : (as bs : CList A) -> as ++ bs  bs ++ as
++-comm = elimCListProp.f _
  (sym  ++-unitr)
   a {as} p bs -> cong (a ∷_) (p bs)  cong (_++ as) (++-∷ a bs)  ++-assocr bs [ a ] as)
  (isPropΠ λ _ -> isSetCList _ _)

clist-α :  {n : Level} {X : Type n} -> sig M.MonSig (CList X) -> CList X
clist-α (M.`e , i) = []
clist-α (M.`⊕ , i) = i fzero ++ i fone

module Free {x y : Level} {A : Type x} {𝔜 : struct y M.MonSig} (isSet𝔜 : isSet (𝔜 .car)) (𝔜-cmon : 𝔜  M.CMonSEq) where
  module 𝔜 = M.CMonSEq 𝔜 𝔜-cmon

  𝔛 : M.CMonStruct
  𝔛 = < CList A , clist-α >

  module _ (f : A -> 𝔜 .car) where
    _♯ : CList A -> 𝔜 .car
    _♯ = elimCListSet.f _
      𝔜.e
       a p -> f a 𝔜.⊕ p)
       a b {ab} {bs} {cs} {as*} {bs*} cs* bp bq ->
        f a 𝔜.⊕ as* ≡⟨ cong (f a 𝔜.⊕_) bp 
        f a 𝔜.⊕ f b 𝔜.⊕ cs* ≡⟨ sym (𝔜.assocr _ _ _) 
        (f a 𝔜.⊕ f b) 𝔜.⊕ cs* ≡⟨ cong (𝔜._⊕ cs*) (𝔜.comm _ _) 
        (f b 𝔜.⊕ f a) 𝔜.⊕ cs* ≡⟨ 𝔜.assocr _ _ _ 
        f b 𝔜.⊕ (f a 𝔜.⊕ cs*) ≡⟨ cong (f b 𝔜.⊕_) (sym bq) 
        f b 𝔜.⊕ bs* 
      )
      isSet𝔜

    private
      ♯-++ :  xs ys -> (xs ++ ys)   (xs ) 𝔜.⊕ (ys )
      ♯-++ = elimCListProp.f _
         ys -> sym (𝔜.unitl (ys )))
         a {xs} p ys ->
          f a 𝔜.⊕ ((xs ++ ys) ) ≡⟨ cong (f a 𝔜.⊕_) (p ys) 
          f a 𝔜.⊕ ((xs ) 𝔜.⊕ (ys )) ≡⟨ sym (𝔜.assocr (f a) (xs ) (ys )) 
          _ 
        )
        (isPropΠ λ _ -> isSet𝔜 _ _)

    ♯-isMonHom : structHom 𝔛 𝔜
    fst ♯-isMonHom = _♯
    snd ♯-isMonHom M.`e i = 𝔜.e-eta
    snd ♯-isMonHom M.`⊕ i = 𝔜.⊕-eta i _♯  sym (♯-++ (i fzero) (i fone))

  private
    clistEquivLemma : (g : structHom 𝔛 𝔜) -> (x : CList A) -> g .fst x  ((g .fst  [_]) ) x
    clistEquivLemma (g , homMonWit) = elimCListProp.f _
      (sym (homMonWit M.`e (lookup L.[]))  𝔜.e-eta)
       x {xs} p ->
        g (x  xs) ≡⟨ sym (homMonWit M.`⊕ (lookup ([ x ] L.∷ xs L.∷ L.[]))) 
        _ ≡⟨ 𝔜.⊕-eta (lookup ([ x ] L.∷ xs L.∷ L.[])) g 
        _ ≡⟨ cong (g [ x ] 𝔜.⊕_) p 
        _ 
      )
      (isSet𝔜 _ _)

    clistEquivLemma-β : (g : structHom 𝔛 𝔜) -> g  ♯-isMonHom (g .fst  [_])
    clistEquivLemma-β g = structHom≡ 𝔛 𝔜 g (♯-isMonHom (g .fst  [_])) isSet𝔜 (funExt (clistEquivLemma g))

  clistMonEquiv : structHom 𝔛 𝔜  (A -> 𝔜 .car)
  clistMonEquiv =
    isoToEquiv (iso  g -> g .fst  [_]) ♯-isMonHom  g -> funExt (𝔜.unitr  g)) (sym  clistEquivLemma-β))

module CListDef = F.Definition M.MonSig M.CMonEqSig M.CMonSEq

clist-sat :  {n} {X : Type n} -> < CList X , clist-α >  M.CMonSEq
clist-sat (M.`mon M.`unitl) ρ = ++-unitl (ρ fzero)
clist-sat (M.`mon M.`unitr) ρ = ++-unitr (ρ fzero)
clist-sat (M.`mon M.`assocr) ρ = ++-assocr (ρ fzero) (ρ fone) (ρ ftwo)
clist-sat M.`comm ρ = ++-comm (ρ fzero) (ρ fone)

clistDef :  { ℓ'} -> CListDef.Free  ℓ' 2
F.Definition.Free.F clistDef = CList
F.Definition.Free.η clistDef = [_]
F.Definition.Free.α clistDef = clist-α
F.Definition.Free.sat clistDef = clist-sat
F.Definition.Free.isFree clistDef isSet𝔜 satMon = (Free.clistMonEquiv isSet𝔜 satMon) .snd