Sequences

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-08-30.
Last modified on 2025-10-31.

module lists.sequences where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.function-types

open import lists.dependent-sequences

Idea

A sequence of elements of type A is a map ℕ → A from the natural numbers into A.

For a list of number sequences from the On-Line Encyclopedia of Integer Sequences [OEIS] that are formalized in agda-unimath, see the page literature.oeis.

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

Binary functorial action on maps of sequences

binary-map-sequence :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} → (A → B → C) →
  sequence A → sequence B → sequence C
binary-map-sequence f a b n = f (a n) (b n)

Pairing two sequences

pair-sequence :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → sequence A → sequence B →
  sequence (A × B)
pair-sequence = binary-map-sequence pair

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.

Recent changes