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β‰₯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 ⚠️ 
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