# Partial sequences

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-12-07.

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