Sequences

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-06.
Last modified on 2024-10-25.

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 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

References

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

Recent changes