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 Agda.Builtin.List 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:

module _ where private
  data List' {β„“} (A : Type β„“) : Type β„“ where
    [] : List' A
    _∷_ : A β†’ List' A β†’ List' A

Path SpaceπŸ”—

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

head : A β†’ List A β†’ A
head def []     = def
head _   (x ∷ _) = x

tail : List A β†’ List A
tail []      = []
tail (_ ∷ xs) = xs

∷-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} β†’ Code xs ys ≃ (xs ≑ ys)
  Code≃Path = Isoβ†’Equiv (decode , iso encode decode-encode encode-decode)

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

We can define concatenation of lists by recursion:

infixr 5 _++_
_++_ : βˆ€ {β„“} {A : Type β„“} β†’ List A β†’ List A β†’ List A
[]      ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

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