Shifting sequences

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

Created on 2022-09-15.
Last modified on 2023-06-08.

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

Recent changes