Functoriality of the type of tuples

Content created by Garrett Figueroa and Louis Wasserman.

Created on 2025-05-14.
Last modified on 2025-10-31.

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. This is the functorial action of tuples.

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