# Functoriality of the type of vectors

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-03-15.

module linear-algebra.functoriality-vectors where

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

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import linear-algebra.vectors

open import univalent-combinatorics.standard-finite-types


## Idea

Any map f : A → B determines a map vec A n → vec B n for every n.

## Definition

### Functoriality of the type of listed vectors

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

map-vec : {n : ℕ} → (A → B) → vec A n → vec B n
map-vec _ empty-vec = empty-vec
map-vec f (x ∷ xs) = f x ∷ map-vec f xs

htpy-vec :
{n : ℕ} {f g : A → B} → (f ~ g) → map-vec {n = n} f ~ map-vec {n = n} g
htpy-vec H empty-vec = refl
htpy-vec H (x ∷ v) = ap-binary _∷_ (H x) (htpy-vec H v)


### Binary functoriality of the type of listed vectors

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
where

binary-map-vec :
{n : ℕ} → (A → B → C) → vec A n → vec B n → vec C n
binary-map-vec f empty-vec empty-vec = empty-vec
binary-map-vec f (x ∷ v) (y ∷ w) = f x y ∷ binary-map-vec f v w


### Functoriality of the type of functional vectors

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

map-functional-vec :
(n : ℕ) → (A → B) → functional-vec A n → functional-vec B n
map-functional-vec n f v = f ∘ v

htpy-functional-vec :
(n : ℕ) {f g : A → B} → (f ~ g) →
map-functional-vec n f ~ map-functional-vec n g
htpy-functional-vec n = htpy-postcomp (Fin n)


### Binary functoriality of the type of functional vectors

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
where

binary-map-functional-vec :
(n : ℕ) → (A → B → C) →
functional-vec A n → functional-vec B n → functional-vec C n
binary-map-functional-vec n f v w i = f (v i) (w i)

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

map-vec-map-functional-vec :
(n : ℕ) (v : vec A n) →
listed-vec-functional-vec
( n)
( map-functional-vec n f (functional-vec-vec n v)) ＝
map-vec f v
map-vec-map-functional-vec zero-ℕ empty-vec = refl
map-vec-map-functional-vec (succ-ℕ n) (x ∷ v) =
eq-Eq-vec
( succ-ℕ n)
( listed-vec-functional-vec
( succ-ℕ n)
( map-functional-vec
( succ-ℕ n)
( f)
( functional-vec-vec (succ-ℕ n) (x ∷ v))))
( map-vec f (x ∷ v))
( refl ,
Eq-eq-vec
( n)
( listed-vec-functional-vec
( n)
( map-functional-vec n f (functional-vec-vec n v)))
( map-vec f v)
( map-vec-map-functional-vec n v))