{-# OPTIONS --cubical --safe #-}

module Container.List.Isomorphism where

open import Prelude
open import Container
open import Container.List
open import Data.Fin
open import Data.List using (tabulate; length ; _!_) renaming (_āˆ·_ to _Lāˆ·_; [] to L[]; List to š•ƒ)
open import Data.List.Properties

ā„’ā†’š•ƒ : List A ā†’ š•ƒ A
ā„’ā†’š•ƒ = uncurry tabulate

š•ƒā†’ā„’ : š•ƒ A ā†’ List A
š•ƒā†’ā„’ xs .fst = length xs
š•ƒā†’ā„’ xs .snd i = xs ! i

ā„’ā†’š•ƒā†’ā„’ : āˆ€ n (xs : Fin n ā†’ A) ā†’ š•ƒā†’ā„’ (ā„’ā†’š•ƒ (n , xs)) ā‰” (n , xs)
ā„’ā†’š•ƒā†’ā„’ n xs i .fst = tab-length n xs i
ā„’ā†’š•ƒā†’ā„’ n xs i .snd = tab-id n xs i

š•ƒā†’ā„’ā†’š•ƒ : āˆ€ (xs : š•ƒ A) ā†’ ā„’ā†’š•ƒ (š•ƒā†’ā„’ xs) ā‰” xs
š•ƒā†’ā„’ā†’š•ƒ L[] _ = L[]
š•ƒā†’ā„’ā†’š•ƒ (x Lāˆ· xs) i = x Lāˆ· š•ƒā†’ā„’ā†’š•ƒ xs i

š•ƒā‡”ā„’ : š•ƒ A ā‡” List A
š•ƒā‡”ā„’ .fun = š•ƒā†’ā„’
š•ƒā‡”ā„’ .inv = ā„’ā†’š•ƒ
š•ƒā‡”ā„’ .rightInv  = uncurry ā„’ā†’š•ƒā†’ā„’
š•ƒā‡”ā„’ .leftInv = š•ƒā†’ā„’ā†’š•ƒ