Lists

module lists.lists where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.maybe
open import foundation.negation
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

Idea

The type of lists of elements of a type A is defined inductively, with an empty list and an operation that extends a list with one element from A.

Definition

The inductive definition of the type of lists

data list {l : Level} (A : UU l) : UU l where
  nil : list A
  cons : A  list A  list A
{-# BUILTIN LIST list #-}

Predicates on the type of lists

is-nil-list : {l : Level} {A : UU l}  list A  UU l
is-nil-list l = (l  nil)

is-nonnil-list : {l : Level} {A : UU l}  list A  UU l
is-nonnil-list l = ¬ (is-nil-list l)

is-cons-list : {l : Level} {A : UU l}  list A  UU l
is-cons-list {l1} {A} l = Σ (A × list A)  (a , l')  l  cons a l')

Operations

Fold

fold-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) (μ : A  (B  B)) 
  list A  B
fold-list b μ nil = b
fold-list b μ (cons a l) = μ a (fold-list b μ l)

The dual of cons

snoc : {l : Level} {A : UU l}  list A  A  list A
snoc nil a = cons a nil
snoc (cons b l) a = cons b (snoc l a)

The unit list

unit-list : {l : Level} {A : UU l}  A  list A
unit-list a = cons a nil

The length of a list

length-list : {l : Level} {A : UU l}  list A  
length-list = fold-list 0  a  succ-ℕ)

The elementhood predicate on lists

data _∈-list_ {l : Level} {A : UU l} : A  list A  UU l where
  is-head : (a : A) (l : list A)  a ∈-list (cons a l)
  is-in-tail : (a x : A) (l : list A)  a ∈-list l  a ∈-list (cons x l)

Properties

A list that uses cons is not nil

is-nonnil-cons-list :
  {l : Level} {A : UU l} 
  (a : A)  (l : list A)  is-nonnil-list (cons a l)
is-nonnil-cons-list a l ()

is-nonnil-is-cons-list :
  {l : Level} {A : UU l} 
  (l : list A)  is-cons-list l  is-nonnil-list l
is-nonnil-is-cons-list l ((a , l') , refl) q =
  is-nonnil-cons-list a l' q

A list that uses cons is not nil

is-cons-is-nonnil-list :
  {l : Level} {A : UU l} 
  (l : list A)  is-nonnil-list l  is-cons-list l
is-cons-is-nonnil-list nil p = ex-falso (p refl)
is-cons-is-nonnil-list (cons x l) p = ((x , l) , refl)

head-is-nonnil-list :
  {l : Level} {A : UU l} 
  (l : list A)  is-nonnil-list l  A
head-is-nonnil-list l p =
  pr1 (pr1 (is-cons-is-nonnil-list l p))

tail-is-nonnil-list :
  {l : Level} {A : UU l} 
  (l : list A)  is-nonnil-list l  list A
tail-is-nonnil-list l p =
  pr2 (pr1 (is-cons-is-nonnil-list l p))

Characterizing the identity type of lists

Eq-list : {l1 : Level} {A : UU l1}  list A  list A  UU l1
Eq-list {l1} nil nil = raise-unit l1
Eq-list {l1} nil (cons x l') = raise-empty l1
Eq-list {l1} (cons x l) nil = raise-empty l1
Eq-list {l1} (cons x l) (cons x' l') = (Id x x') × Eq-list l l'

refl-Eq-list : {l1 : Level} {A : UU l1} (l : list A)  Eq-list l l
refl-Eq-list nil = raise-star
refl-Eq-list (cons x l) = pair refl (refl-Eq-list l)

Eq-eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A)  Id l l'  Eq-list l l'
Eq-eq-list l .l refl = refl-Eq-list l

eq-Eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A)  Eq-list l l'  Id l l'
eq-Eq-list nil nil (map-raise star) = refl
eq-Eq-list nil (cons x l') (map-raise f) = ex-falso f
eq-Eq-list (cons x l) nil (map-raise f) = ex-falso f
eq-Eq-list (cons x l) (cons .x l') (pair refl e) =
  ap (cons x) (eq-Eq-list l l' e)

square-eq-Eq-list :
  {l1 : Level} {A : UU l1} {x : A} {l l' : list A} (p : Id l l') 
  Id (Eq-eq-list (cons x l) (cons x l') (ap (cons x) p))
     (pair refl (Eq-eq-list l l' p))
square-eq-Eq-list refl = refl

issec-eq-Eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A) (e : Eq-list l l') 
  Id (Eq-eq-list l l' (eq-Eq-list l l' e)) e
issec-eq-Eq-list nil nil e = eq-is-contr is-contr-raise-unit
issec-eq-Eq-list nil (cons x l') e = ex-falso (is-empty-raise-empty e)
issec-eq-Eq-list (cons x l) nil e = ex-falso (is-empty-raise-empty e)
issec-eq-Eq-list (cons x l) (cons .x l') (pair refl e) =
  ( square-eq-Eq-list (eq-Eq-list l l' e)) 
  ( ap (pair refl) (issec-eq-Eq-list l l' e))

eq-Eq-refl-Eq-list :
  {l1 : Level} {A : UU l1} (l : list A) 
  Id (eq-Eq-list l l (refl-Eq-list l)) refl
eq-Eq-refl-Eq-list nil = refl
eq-Eq-refl-Eq-list (cons x l) = ap (ap (cons x)) (eq-Eq-refl-Eq-list l)

isretr-eq-Eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A) (p : Id l l') 
  Id (eq-Eq-list l l' (Eq-eq-list l l' p)) p
isretr-eq-Eq-list nil .nil refl = refl
isretr-eq-Eq-list (cons x l) .(cons x l) refl = eq-Eq-refl-Eq-list (cons x l)

is-equiv-Eq-eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A)  is-equiv (Eq-eq-list l l')
is-equiv-Eq-eq-list l l' =
  is-equiv-has-inverse
    ( eq-Eq-list l l')
    ( issec-eq-Eq-list l l')
    ( isretr-eq-Eq-list l l')

equiv-Eq-list :
  {l1 : Level} {A : UU l1} (l l' : list A)  Id l l'  Eq-list l l'
equiv-Eq-list l l' =
  pair (Eq-eq-list l l') (is-equiv-Eq-eq-list l l')

is-contr-total-Eq-list :
  {l1 : Level} {A : UU l1} (l : list A) 
  is-contr (Σ (list A) (Eq-list l))
is-contr-total-Eq-list {A = A} l =
  is-contr-equiv'
    ( Σ (list A) (Id l))
    ( equiv-tot (equiv-Eq-list l))
    ( is-contr-total-path l)

is-trunc-Eq-list :
  (k : 𝕋) {l : Level} {A : UU l}  is-trunc (succ-𝕋 (succ-𝕋 k)) A 
  (l l' : list A)  is-trunc (succ-𝕋 k) (Eq-list l l')
is-trunc-Eq-list k H nil nil =
  is-trunc-is-contr (succ-𝕋 k) is-contr-raise-unit
is-trunc-Eq-list k H nil (cons x l') =
  is-trunc-is-empty k is-empty-raise-empty
is-trunc-Eq-list k H (cons x l) nil =
  is-trunc-is-empty k is-empty-raise-empty
is-trunc-Eq-list k H (cons x l) (cons y l') =
  is-trunc-prod (succ-𝕋 k) (H x y) (is-trunc-Eq-list k H l l')

is-trunc-list :
  (k : 𝕋) {l : Level} {A : UU l}  is-trunc (succ-𝕋 (succ-𝕋 k)) A 
  is-trunc (succ-𝕋 (succ-𝕋 k)) (list A)
is-trunc-list k H l l' =
  is-trunc-equiv
    ( succ-𝕋 k)
    ( Eq-list l l')
    ( equiv-Eq-list l l')
    ( is-trunc-Eq-list k H l l')

is-set-list :
  {l : Level} {A : UU l}  is-set A  is-set (list A)
is-set-list = is-trunc-list neg-two-𝕋

list-Set : {l : Level}  Set l  Set l
list-Set A = pair (list (type-Set A)) (is-set-list (is-set-type-Set A))

The length operation behaves well with respect to the other list operations

length-nil :
  {l1 : Level} {A : UU l1} 
  Id (length-list {A = A} nil) zero-ℕ
length-nil = refl

is-nil-is-zero-length-list :
  {l1 : Level} {A : UU l1}
  (l : list A) 
  is-zero-ℕ (length-list l) 
  is-nil-list l
is-nil-is-zero-length-list nil p = refl

is-nonnil-is-nonzero-length-list :
  {l1 : Level} {A : UU l1}
  (l : list A) 
  is-nonzero-ℕ (length-list l) 
  is-nonnil-list l
is-nonnil-is-nonzero-length-list nil p q = p refl
is-nonnil-is-nonzero-length-list (cons x l) p ()

is-nonzero-length-is-nonnil-list :
  {l1 : Level} {A : UU l1}
  (l : list A) 
  is-nonnil-list l 
  is-nonzero-ℕ (length-list l)
is-nonzero-length-is-nonnil-list nil p q = p refl

lenght-tail-is-nonnil-list :
  {l1 : Level} {A : UU l1}
  (l : list A)  (p : is-nonnil-list l) 
  succ-ℕ (length-list (tail-is-nonnil-list l p)) 
    length-list l
lenght-tail-is-nonnil-list nil p = ex-falso (p refl)
lenght-tail-is-nonnil-list (cons x l) p = refl

Head and tail operations

We define the head and tail operations, and we define the operations of picking and removing the last element from a list.

head-snoc-list :
  {l : Level} {A : UU l} (l : list A)  A  A
head-snoc-list nil a = a
head-snoc-list (cons h l) a = h

head-list :
  {l1 : Level} {A : UU l1}  list A  list A
head-list nil = nil
head-list (cons a x) = unit-list a

tail-list :
  {l1 : Level} {A : UU l1}  list A  list A
tail-list nil = nil
tail-list (cons a x) = x

last-element-list :
  {l1 : Level} {A : UU l1}  list A  list A
last-element-list nil = nil
last-element-list (cons a nil) = unit-list a
last-element-list (cons a (cons b x)) = last-element-list (cons b x)

Removing the last element of a list

remove-last-element-list :
  {l1 : Level} {A : UU l1}  list A  list A
remove-last-element-list nil = nil
remove-last-element-list (cons a nil) = nil
remove-last-element-list (cons a (cons b x)) =
  cons a (remove-last-element-list (cons b x))

Properties of heads and tails and their duals

head-snoc-snoc-list :
  {l1 : Level} {A : UU l1} (x : list A) (a : A) (b : A) 
  head-list (snoc (snoc x a) b)  head-list (snoc x a)
head-snoc-snoc-list nil a b = refl
head-snoc-snoc-list (cons c x) a b = refl

tail-snoc-snoc-list :
  {l1 : Level} {A : UU l1} (x : list A) (a : A) (b : A) 
  tail-list (snoc (snoc x a) b)  snoc (tail-list (snoc x a)) b
tail-snoc-snoc-list nil a b = refl
tail-snoc-snoc-list (cons c x) a b = refl

last-element-snoc :
  {l1 : Level} {A : UU l1} (x : list A) (a : A) 
  Id (last-element-list (snoc x a)) (unit-list a)
last-element-snoc nil a = refl
last-element-snoc (cons b nil) a = refl
last-element-snoc (cons b (cons c x)) a =
  last-element-snoc (cons c x) a

Algebra structure on the type of lists of elements of A

map-algebra-list :
  {l1 : Level} (A : UU l1) 
  Maybe (A × list A)  list A
map-algebra-list A (inl (a , x)) = cons a x
map-algebra-list A (inr star) = nil

inv-map-algebra-list :
  {l1 : Level} (A : UU l1) 
  list A  Maybe (A × list A)
inv-map-algebra-list A nil = inr star
inv-map-algebra-list A (cons a x) = inl (pair a x)

issec-inv-map-algebra-list :
  {l1 : Level} (A : UU l1) 
  (map-algebra-list A  inv-map-algebra-list A) ~ id
issec-inv-map-algebra-list A nil = refl
issec-inv-map-algebra-list A (cons a x) = refl

isretr-inv-map-algebra-list :
  {l1 : Level} (A : UU l1) 
  (inv-map-algebra-list A  map-algebra-list A) ~ id
isretr-inv-map-algebra-list A (inl (a , x)) = refl
isretr-inv-map-algebra-list A (inr star) = refl

is-equiv-map-algebra-list :
  {l1 : Level} (A : UU l1)  is-equiv (map-algebra-list A)
is-equiv-map-algebra-list A =
  is-equiv-has-inverse
    ( inv-map-algebra-list A)
    ( issec-inv-map-algebra-list A)
    ( isretr-inv-map-algebra-list A)