# Functoriality of the list operation

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-04-08.

module lists.functoriality-lists where

Imports
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.transport-along-identifications
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)