Partial sequences

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.
Last modified on 2024-01-28.

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

open import foundation.partial-functions
open import foundation.universe-levels

open import foundation-core.propositions

Idea

A partial sequence of elements of a type A is a partial function from ℕ to A. In other words, a partial sequence is a map

  ℕ → Σ (P : Prop), (P → A)

from ℕ into the type of partial elements of A.

Definitions

Partial sequences

partial-sequence : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
partial-sequence l2 A = partial-function l2 ℕ A

Defined elements of partial sequences

module _
  {l1 l2 : Level} {A : UU l1} (a : partial-sequence l2 A)
  where

  is-defined-prop-partial-sequence : ℕ → Prop l2
  is-defined-prop-partial-sequence = is-defined-prop-partial-function a

  is-defined-partial-sequence : ℕ → UU l2
  is-defined-partial-sequence = is-defined-partial-function a

Recent changes