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

open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base
open import Data.Id.Base
open import Data.Bool

open import Meta.Idiom

module Data.List where

open import Data.List.Base public
open import Data.List.Membership 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π

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 \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 β οΈ
map-id
: β {β} {A : Type β}
β (xs : List A)
β map id xs β‘ xs
map-id [] = refl
map-id (x β· xs) = ap (x β·_) (map-id xs)

map-++
: β {β β'} {A : Type β} {B : Type β'}
β (f : A β B)
β (xs ys : List A)
β map f (xs ++ ys) β‘ map f xs ++ map f ys
map-++ f [] ys = refl
map-++ f (x β· xs) ys = ap (f x β·_) (map-++ f xs ys)

take-length : β {β} {A : Type β} (xs : List A) β take (length xs) xs β‘ xs
take-length [] = refl
take-length (x β· xs) = ap (x β·_) (take-length xs)

take-length-more
: β {β} {A : Type β} (xs : List A) (n : Nat)
β length xs β€ n
β take n xs β‘ xs
take-length-more [] zero wit = refl
take-length-more [] (suc n) wit = refl
take-length-more (x β· xs) (suc n) (sβ€s wit) = ap (x β·_) (take-length-more xs n wit)

all-of-++
: β {β} {A : Type β}
β (f : A β Bool)
β (xs ys : List A)
β all-of f (xs ++ ys) β‘ and (all-of f xs) (all-of f ys)
all-of-++ f [] ys = refl
all-of-++ f (x β· xs) ys =
ap (and (f x)) (all-of-++ f xs ys)
β and-associative (f x) (all-of f xs) (all-of f ys)

all-of-map
: β {β β'} {A : Type β} {B : Type β'}
β (f : B β Bool)
β (g : A β B)
β (xs : List A)
β all-of f (map g xs) β‘ all-of (f β g) xs
all-of-map f g [] = refl
all-of-map f g (x β· xs) = ap (and (f (g x))) (all-of-map f g xs)

any-of-++
: β {β} {A : Type β}
β (f : A β Bool)
β (xs ys : List A)
β any-of f (xs ++ ys) β‘ or (any-of f xs) (any-of f ys)
any-of-++ f [] ys = refl
any-of-++ f (x β· xs) ys =
ap (or (f x)) (any-of-++ f xs ys)
β or-associative (f x) (any-of f xs) (any-of f ys)

any-of-map
: β {β β'} {A : Type β} {B : Type β'}
β (f : B β Bool)
β (g : A β B)
β (xs : List A)
β any-of f (map g xs) β‘ any-of (f β g) xs
any-of-map f g [] = refl
any-of-map f g (x β· xs) = ap (or (f (g x))) (any-of-map f g xs)

all-of-or
: β {β} {A : Type β}
β (f : A β Bool)
β (b : Bool) (xs : List A)
β all-of (Ξ» x β or b (f x)) xs β‘ or b (all-of f xs)
all-of-or f b [] = sym (or-truer b)
all-of-or f b (x β· xs) =
ap (and (or b (f x))) (all-of-or f b xs)
β sym (or-distrib-andl b (f x) (all-of f xs))

not-all-of
: β {β} {A : Type β}
β (f : A β Bool)
β (xs : List A)
β not (all-of f xs) β‘ any-of (not β f) xs
not-all-of f [] = refl
not-all-of f (x β· xs) =
not-andβ‘or-not (f x) (all-of f xs)
β ap (or (not (f x))) (not-all-of f xs)

not-any-of
: β {β} {A : Type β}
β (f : A β Bool)
β (xs : List A)
β not (any-of f xs) β‘ all-of (not β f) xs
not-any-of f [] = refl
not-any-of f (x β· xs) =
not-orβ‘and-not (f x) (any-of f xs)
β ap (and (not (f x))) (not-any-of f xs)

any-one-of
: β {β} {A : Type β}
β (f : A β Bool)
β (x : A) (xs : List A)
β x ββ xs β f x β‘ true
β any-of f xs β‘ true
any-one-of f x (y β· xs) (here x=y) x-true =
apβ or (subst (Ξ» e β f e β‘ true) x=y x-true) refl
any-one-of f x (y β· xs) (there xβxs) x-true =
apβ or refl (any-one-of f x xs xβxs x-true) β or-truer _

is-empty : List A β Type
is-empty [] = β€
is-empty (_ β· _) = β₯

is-empty? : β (xs : List A) β Dec (is-empty xs)
is-empty? [] = yes tt
is-empty? (x β· xs) = no id