Shifting sequences

module foundation.shifting-sequences where

open import elementary-number-theory.natural-numbers

open import foundation-core.universe-levels

Idea

Given a sequence f : ℕ → A and an element a : A we define shift-ℕ a f : ℕ → A by

  shift-ℕ a f zero-ℕ := a
  shift-ℕ a f (succ-ℕ n) := f n

Definition

shift-ℕ : {l : Level} {A : UU l} (a : A) (f : ℕ → A) → ℕ → A
shift-ℕ a f zero-ℕ = a
shift-ℕ a f (succ-ℕ n) = f n