Functoriality of the list operation

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

open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors

open import lists.arrays
open import lists.concatenation-lists
open import lists.lists

Idea

Given a functiion f : A → B, we obtain a function map-list f : list A → list B.

Definition

map-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
  list A  list B
map-list f = fold-list nil  a  cons (f a))

Properties

map-list preserves the length of a list

length-map-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) (l : list A) 
  Id (length-list (map-list f l)) (length-list l)
length-map-list f nil = refl
length-map-list f (cons x l) =
  ap succ-ℕ (length-map-list f l)
module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (f : A  B)
  where

  map-list-map-vec-list :
    (l : list A) 
    list-vec (length-list l) (map-vec f (vec-list l)) 
    map-list f l
  map-list-map-vec-list nil = refl
  map-list-map-vec-list (cons x l) =
    eq-Eq-list
      ( list-vec (length-list (cons x l)) (map-vec f (vec-list (cons x l))))
      ( map-list f (cons x l))
      ( refl ,
        Eq-eq-list
          ( list-vec (length-list l) (map-vec f (vec-list l)))
          ( map-list f l)
          ( map-list-map-vec-list l))

  map-vec-map-list-vec :
    (n : ) (v : vec A n) 
    tr
      ( vec B)
      ( length-map-list f (list-vec n v) 
        compute-length-list-list-vec n v)
      ( vec-list (map-list f (list-vec n v))) 
    map-vec f v
  map-vec-map-list-vec 0 empty-vec = refl
  map-vec-map-list-vec (succ-ℕ n) (x  v) =
    compute-tr-vec
      ( ap succ-ℕ (length-map-list f (list-vec n v)) 
        compute-length-list-list-vec (succ-ℕ n) (x  v))
      ( vec-list (fold-list nil  a  cons (f a)) (list-vec n v)))
      ( f x) 
    eq-Eq-vec
      ( succ-ℕ n)
      ( f x 
        tr
          ( vec B)
          ( is-injective-succ-ℕ
            ( ap succ-ℕ (length-map-list f (list-vec n v)) 
              compute-length-list-list-vec (succ-ℕ n) (x  v)))
          ( vec-list (map-list f (list-vec n v))))
      ( map-vec f (x  v))
      ( refl ,
        ( Eq-eq-vec
          ( n)
          ( tr
            ( vec B)
            ( is-injective-succ-ℕ
              ( ap succ-ℕ (length-map-list f (list-vec n v)) 
                compute-length-list-list-vec (succ-ℕ n) (x  v)))
            ( vec-list (map-list f (list-vec n v))))
          ( map-vec f v)
          ( tr
            ( λ p 
              tr
                ( vec B)
                ( p)
                ( vec-list (map-list f (list-vec n v))) 
               map-vec f v)
            ( eq-is-prop
              ( is-set-ℕ
                ( length-list (map-list f (list-vec n v)))
                ( n)))
            ( map-vec-map-list-vec n v))))

  map-vec-map-list-vec' :
    (n : ) (v : vec A n) 
    vec-list (map-list f (list-vec n v)) 
    tr
      ( vec B)
      ( inv
        ( length-map-list f (list-vec n v) 
          compute-length-list-list-vec n v))
      ( map-vec f v)
  map-vec-map-list-vec' n v =
    eq-transpose-tr'
      ( length-map-list f (list-vec n v)  compute-length-list-list-vec n v)
      ( map-vec-map-list-vec n v)

  vec-list-map-list-map-vec-list :
    (l : list A) 
    tr
      ( vec B)
      ( length-map-list f l)
      ( vec-list (map-list f l)) 
    map-vec f (vec-list l)
  vec-list-map-list-map-vec-list nil = refl
  vec-list-map-list-map-vec-list (cons x l) =
    compute-tr-vec
      ( ap succ-ℕ (length-map-list f l))
      ( vec-list (map-list f l))
      ( f x) 
    eq-Eq-vec
      ( succ-ℕ (length-list l))
      ( f x 
        tr
          ( vec B)
          ( is-injective-succ-ℕ (ap succ-ℕ (length-map-list f l)))
          ( vec-list (map-list f l)))
      ( map-vec f (vec-list (cons x l)))
      ( refl ,
        Eq-eq-vec
          ( length-list l)
          ( tr
            ( vec B)
            ( is-injective-succ-ℕ (ap succ-ℕ (length-map-list f l)))
            ( vec-list (map-list f l)))
          ( map-vec f (vec-list l))
          ( tr
            ( λ p 
              ( tr
                ( vec B)
                ( p)
                ( vec-list (map-list f l))) 
              ( map-vec f (vec-list l)))
            ( eq-is-prop
              ( is-set-ℕ (length-list (map-list f l)) (length-list l)))
            ( vec-list-map-list-map-vec-list l)))

  vec-list-map-list-map-vec-list' :
    (l : list A) 
    vec-list (map-list f l) 
    tr
      ( vec B)
      ( inv (length-map-list f l))
      ( map-vec f (vec-list l))
  vec-list-map-list-map-vec-list' l =
    eq-transpose-tr'
      ( length-map-list f l)
      ( vec-list-map-list-map-vec-list l)

  list-vec-map-vec-map-list-vec :
    (n : ) (v : vec A n) 
    list-vec
      ( length-list (map-list f (list-vec n v)))
      ( vec-list (map-list f (list-vec n v))) 
    list-vec n (map-vec f v)
  list-vec-map-vec-map-list-vec n v =
    ap
      ( λ p  list-vec (pr1 p) (pr2 p))
      ( eq-pair-Σ
        ( length-map-list f (list-vec n v) 
          compute-length-list-list-vec n v)
        ( map-vec-map-list-vec n v))

map-list preserves concatenation

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)
  where

  preserves-concat-map-list :
    (l k : list A) 
    Id ( map-list f (concat-list l k))
       ( concat-list (map-list f l) (map-list f k))
  preserves-concat-map-list nil k = refl
  preserves-concat-map-list (cons x l) k =
    ap (cons (f x)) (preserves-concat-map-list l k)

Functoriality of the list operation

First we introduce the functoriality of the list operation, because it will come in handy when we try to define and prove more advanced things.

identity-law-map-list :
  {l1 : Level} {A : UU l1} 
  map-list (id {A = A}) ~ id
identity-law-map-list nil = refl
identity-law-map-list (cons a x) =
  ap (cons a) (identity-law-map-list x)

composition-law-map-list :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} 
  (f : A  B) (g : B  C) 
  map-list (g  f) ~ (map-list g  map-list f)
composition-law-map-list f g nil = refl
composition-law-map-list f g (cons a x) =
  ap (cons (g (f a))) (composition-law-map-list f g x)

map-list applied to lists of the form snoc x a

map-snoc-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) (x : list A) (a : A) 
  map-list f (snoc x a)  snoc (map-list f x) (f a)
map-snoc-list f nil a = refl
map-snoc-list f (cons b x) a = ap (cons (f b)) (map-snoc-list f x a)