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

Shifting sequences

module foundation.shifting-sequences where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.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