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


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 (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} β¦ 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))