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