open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Universe
open import 1Lab.HLevel.Closure
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.List.Base
open import Data.Dec.Base
open import Data.Fin.Base using (Fin ; fzero ; fsuc)
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.Properties where

headerπŸ”—

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 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 = Equivβ†’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 (lower x)
    Code-is-hlevel {x ∷ x₁} {[]}     = is-propβ†’is-hlevel-suc Ξ» x β†’ absurd (lower x)
    Code-is-hlevel {x ∷ x₁} {xβ‚‚ ∷ y} = Γ—-is-hlevel (suc n) (ahl _ _) Code-is-hlevel

  instance
    H-Level-List : βˆ€ {n} ⦃ p : 2 ≀ n ⦄ ⦃ _ : H-Level A n ⦄ β†’ H-Level (List A) n
    H-Level-List {n = suc (suc n)} ⦃ s≀s (s≀s p) ⦄ ⦃ x ⦄ =
      record { has-hlevel = 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

_ : βˆ€ {β„“} {A : n-Type β„“ 2} β†’ is-hlevel (List ∣ A ∣) 5
_ = hlevel 5

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)

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

length-tabulate : βˆ€ {n} (f : Fin n β†’ A) β†’ length (tabulate f) ≑ n
length-tabulate {n = zero}  f = refl
length-tabulate {n = suc n} f = ap suc (length-tabulate (f ∘ fsuc))