Functoriality of the type of tuples
Content created by Garrett Figueroa and Louis Wasserman.
Created on 2025-05-14.
Last modified on 2025-09-05.
module lists.functoriality-tuples 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 lists.tuples open import univalent-combinatorics.standard-finite-types
Idea
Any map f : A → B
determines a map between tuples
tuple A n → tuple B n
for every n
.
Definition
Functoriality of the type of tuples
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where map-tuple : {n : ℕ} → (A → B) → tuple A n → tuple B n map-tuple _ empty-tuple = empty-tuple map-tuple f (x ∷ xs) = f x ∷ map-tuple f xs htpy-tuple : {n : ℕ} {f g : A → B} → (f ~ g) → map-tuple {n = n} f ~ map-tuple {n = n} g htpy-tuple H empty-tuple = refl htpy-tuple H (x ∷ v) = ap-binary _∷_ (H x) (htpy-tuple H v)
Binary functoriality of the type of listed tuples
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where binary-map-tuple : {n : ℕ} → (A → B → C) → tuple A n → tuple B n → tuple C n binary-map-tuple f empty-tuple empty-tuple = empty-tuple binary-map-tuple f (x ∷ v) (y ∷ w) = f x y ∷ binary-map-tuple f v w
Properties
The action on maps of tuples preserves identity maps
preserves-id-map-tuple : {l : Level} (n : ℕ) {A : UU l} (x : tuple A n) → x = map-tuple id x preserves-id-map-tuple zero-ℕ empty-tuple = refl preserves-id-map-tuple (succ-ℕ n) (x ∷ xs) = eq-Eq-tuple ( succ-ℕ n) ( x ∷ xs) ( map-tuple id (x ∷ xs)) ( refl , Eq-eq-tuple n xs (map-tuple id xs) (preserves-id-map-tuple n xs))
The action on maps of tuples preserves composition
preserves-comp-map-tuple : {l1 l2 l3 : Level} (n : ℕ) {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B) (g : B → C) (x : tuple A n) → map-tuple g (map-tuple f x) = map-tuple (g ∘ f) x preserves-comp-map-tuple zero-ℕ f g empty-tuple = refl preserves-comp-map-tuple (succ-ℕ n) f g (x ∷ xs) = eq-Eq-tuple ( succ-ℕ n) ( map-tuple g (map-tuple f (x ∷ xs))) ( map-tuple (g ∘ f) (x ∷ xs)) ( refl , Eq-eq-tuple n ( map-tuple g (map-tuple f xs)) ( map-tuple (g ∘ f) xs) ( preserves-comp-map-tuple n f g xs))
Recent changes
- 2025-09-05. Garrett Figueroa. Category of algebras of a theory (#1483).
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).