Dependent sequences

Content created by Fredrik Bakke.

Created on 2023-10-12.
Last modified on 2023-10-12.

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

open import foundation.universe-levels

open import foundation-core.function-types

Idea

A dependent sequence of elements in a family of types A : ℕ → UU is a dependent map (n : ℕ) → A n.

Definition

Dependent sequences of elements in a family of types

dependent-sequence : {l : Level} → (ℕ → UU l) → UU l
dependent-sequence B = (n : ℕ) → B n

Functorial action on maps of dependent sequences

map-dependent-sequence :
  {l1 l2 : Level} {A : ℕ → UU l1} {B : ℕ → UU l2} →
  ((n : ℕ) → A n → B n) → dependent-sequence A → dependent-sequence B
map-dependent-sequence f a = map-Π f a

Recent changes