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:
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
,
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
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