This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Sequences

module foundation.sequences where

Imports

open import foundation.dependent-sequences
open import foundation.universe-levels

open import foundation-core.function-types

Idea

A sequence of elements in a type A is a map ℕ → A.

Definition

Sequences of elements of a type

sequence : {l : Level} → UU l → UU l
sequence A = dependent-sequence (λ _ → A)

Functorial action on maps of sequences

map-sequence :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → sequence A → sequence B
map-sequence f a = f ∘ a