Shifting sequences

Content created by Fredrik Bakke and Louis Wasserman.

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

module lists.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

Recent changes