Experiments.ListArray

module Experiments.ListArray where

open import Cubical.Data.Sigma
open import Cubical.Data.List renaming (_∷_ to _∷ₗ_)
open import Cubical.Data.Fin
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sum as ⊎
open import Cubical.Induction.WellFounded
import Cubical.Data.Empty as ⊥

import Cubical.Structures.Set.Mon.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

open import Cubical.Structures.Set.Mon.Array
open import Cubical.Structures.Set.Mon.List

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

open Iso

private
  variable
    ℓ : Level
    A : Type ℓ

an-array : Array ℕ
an-array = 3 , lemma
  where
  lemma : Fin 3 -> ℕ
  lemma (0 , p) = 5
  lemma (1 , p) = 9
  lemma (2 , p) = 2
  lemma (suc (suc (suc n)) , p) = ⊥.rec (¬-<-zero (<-k+-cancel p))

module MonDef = F.Definition M.MonSig M.MonEqSig M.MonSEq

want : List ℕ
want = 5 ∷ₗ 9 ∷ₗ 2 ∷ₗ []

to-list : structHom < Array ℕ , arrayA > < List ℕ , listΑ >
to-list = MonDef.Free.ext arrayDef (isOfHLevelList 0 isSetℕ) listSat [_]

_ : to-list .fst an-array ≡ want
_ = refl

to-list' : structHom < Array ℕ , MonDef.Free.α (arrayDef' {ℓ' = ℓ-zero}) > < List ℕ , listΑ >
to-list' = MonDef.Free.ext arrayDef' (isOfHLevelList 0 isSetℕ) listSat [_]

_ : to-list' .fst an-array ≡ want
_ = refl

to-list'' : Array ℕ -> List ℕ
to-list'' = MonDef.freeIso arrayDef listDef isSetℕ .fun

_ : to-list'' an-array ≡ want
_ = refl