open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Bool

module Data.List where

open import Data.List.Base public

ListsπŸ”—

A list is a finite, ordered sequence of elements of some type. Lists are an inductive type, as an Agda builtin. Here, we echo the definition for clarity:

private variable
  β„“ : Level
  A B : Type β„“

Path SpaceπŸ”—

We begin by characteristing the behaviour of paths of lists. For instance, ∷ is injective in both its arguments:

∷-head-inj : βˆ€ {x y : A} {xs ys} β†’ (x ∷ xs) ≑ (y ∷ ys) β†’ x ≑ y
∷-head-inj {x = x} p = ap (head x) p

∷-tail-inj : βˆ€ {x y : A} {xs ys} β†’ (x ∷ xs) ≑ (y ∷ ys) β†’ xs ≑ ys
∷-tail-inj p = ap tail p

Similarly, it is possible to distinguish _ ∷ _ from [], so they are not identical:

βˆ·β‰ [] : βˆ€ {x : A} {xs} β†’ Β¬ (x ∷ xs) ≑ []
βˆ·β‰ [] {A = A} p = subst distinguish p tt where
  distinguish : List A β†’ Type
  distinguish []     = βŠ₯
  distinguish (_ ∷ _) = ⊀

Using these lemmas, we can characterise the path space of List A in terms of the path space of A. For this, we define by induction a type family Code, which represents paths in List A by iterated products of paths in A.

module ListPath {A : Type β„“} where
  Code : List A β†’ List A β†’ Type (level-of A)
  Code [] []             = Lift (level-of A) ⊀
  Code [] (x ∷ x₁)       = Lift (level-of A) βŠ₯
  Code (h ∷ t) []        = Lift (level-of A) βŠ₯
  Code (h ∷ t) (h' ∷ t') = (h ≑ h') Γ— Code t t'

We have a map encode which turns a path into a Code, and a function decode which does the opposite.

  encode : {xs ys : List A} β†’ xs ≑ ys β†’ Code xs ys
  encode {xs = []} {ys = []} path = lift tt
  encode {xs = []} {ys = x ∷ ys} path = lift (βˆ·β‰ [] (sym path))
  encode {xs = x ∷ xs} {ys = []} path = lift (βˆ·β‰ [] path)
  encode {xs = x ∷ xs} {ys = x₁ ∷ ys} path =
    ∷-head-inj path , encode {xs = xs} {ys = ys} (ap tail path)

  decode : {xs ys : List A} β†’ Code xs ys β†’ xs ≑ ys
  decode {[]} {[]} code = refl
  decode {x ∷ xs} {x₁ ∷ ys} (p , q) i = p i ∷ decode q i

These maps are inverses by construction:

  encode-decode : {xs ys : List A} (p : Code xs ys) β†’ encode (decode p) ≑ p
  encode-decode {[]} {[]} (lift tt) = refl
  encode-decode {x ∷ xs} {x₁ ∷ ys} (p , q) i = p , encode-decode q i

  decode-encode : {xs ys : List A} (p : xs ≑ ys) β†’ decode (encode p) ≑ p
  decode-encode = J (Ξ» y p β†’ decode (encode p) ≑ p) de-refl where
    de-refl : {xs : List A} β†’ decode (encode (Ξ» i β†’ xs)) ≑ (Ξ» i β†’ xs)
    de-refl {[]}         = refl
    de-refl {x ∷ xs} i j = x ∷ de-refl {xs = xs} i j

  Code≃Path : {xs ys : List A} β†’ (xs ≑ ys) ≃ Code xs ys
  Code≃Path = Isoβ†’Equiv (encode , iso decode encode-decode decode-encode)

Thus we have a characterisation of Path (List A) in terms of Path A. We use this to prove that lists preserve h-levels for nβ‰₯2n \ge 2, i.e.Β if A is a set (or more) then List A is a type of the same h-level.

  List-is-hlevel : (n : Nat) β†’ is-hlevel A (2 + n) β†’ is-hlevel (List A) (2 + n)
  List-is-hlevel n ahl x y = is-hlevel≃ (suc n) Code≃Path Code-is-hlevel where
    Code-is-hlevel : {x y : List A} β†’ is-hlevel (Code x y) (suc n)
    Code-is-hlevel {[]} {[]}         = is-prop→is-hlevel-suc λ x y → refl
    Code-is-hlevel {[]} {x ∷ y}      = is-propβ†’is-hlevel-suc Ξ» x β†’ absurd (Lift.lower x)
    Code-is-hlevel {x ∷ x₁} {[]}     = is-propβ†’is-hlevel-suc Ξ» x β†’ absurd (Lift.lower x)
    Code-is-hlevel {x ∷ x₁} {xβ‚‚ ∷ y} = Γ—-is-hlevel (suc n) (ahl _ _) Code-is-hlevel

  instance
    H-Level-List : βˆ€ {n} {k} β†’ ⦃ H-Level A (2 + n) ⦄ β†’ H-Level (List A) (2 + n + k)
    H-Level-List {n = n} ⦃ x ⦄ =
      basic-instance (2 + n) (List-is-hlevel n (H-Level.has-hlevel x))

  is-set→List-is-set : is-set A → is-set (List A)
  is-set→List-is-set = List-is-hlevel zero

Then we can prove that this operation is associative and has [] as both left and right units:

++-assoc : βˆ€ {β„“} {A : Type β„“} (xs ys zs : List A)
         β†’ (xs ++ ys) ++ zs ≑ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs i = x ∷ ++-assoc xs ys zs i

++-idl : βˆ€ {β„“} {A : Type β„“} (xs : List A) β†’ [] ++ xs ≑ xs
++-idl xs i = xs

++-idr : βˆ€ {β„“} {A : Type β„“} (xs : List A) β†’ xs ++ [] ≑ xs
++-idr [] i = []
++-idr (x ∷ xs) i = x ∷ ++-idr xs i

LemmasπŸ”—

Continuing with the useful lemmas, if the heads and tails of two lists are identified, then the lists themselves are identified:

ap-∷ : βˆ€ {x y : A} {xs ys : List A}
     β†’ x ≑ y β†’ xs ≑ ys
     β†’ Path (List A) (x ∷ xs) (y ∷ ys)
ap-∷ x≑y xs≑ys i = x≑y i ∷ xs≑ys i
⚠️ TODO: Explain these ⚠️ 
mapUp : (Nat β†’ A β†’ B) β†’ Nat β†’ List A β†’ List B
mapUp f _ [] = []
mapUp f n (x ∷ xs) = f n x ∷ mapUp f (suc n) xs

length : List A β†’ Nat
length [] = zero
length (x ∷ x₁) = suc (length x₁)

concat : List (List A) β†’ List A
concat [] = []
concat (x ∷ xs) = x ++ concat xs

reverse : List A β†’ List A
reverse = go [] where
  go : List A β†’ List A β†’ List A
  go acc [] = acc
  go acc (x ∷ xs) = go (x ∷ acc) xs

_∷r_ : List A β†’ A β†’ List A
xs ∷r x = xs ++ (x ∷ [])

all=? : (A β†’ A β†’ Bool) β†’ List A β†’ List A β†’ Bool
all=? eq=? [] [] = true
all=? eq=? [] (x ∷ ys) = false
all=? eq=? (x ∷ xs) [] = false
all=? eq=? (x ∷ xs) (y ∷ ys) = and (eq=? x y) (all=? eq=? xs ys)

enumerate : βˆ€ {β„“} {A : Type β„“} β†’ List A β†’ List (Nat Γ— A)
enumerate = go 0 where
  go : Nat β†’ List _ β†’ List (Nat Γ— _)
  go x [] = []
  go x (a ∷ b) = (x , a) ∷ go (suc x) b