# Homotopy Type Theory sequentially Hausdorff space > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

# Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

## Definition

### In set theory

Let $S$ be a sequential convergence space. Then $S$ is a sequentially Hausdorff space if for all sequences $x \in S^\mathbb{N}$, the set of all limits of $x$ has at most one element

$isSequentiallyHausdorff(S) \coloneqq \forall x \in S^\mathbb{N}. \{l \in S \vert isLimit_S(x, l)\} \cong \emptyset \vee \{l \in S \vert isLimit_S(x, l)\} \cong \mathbb{1}$

where $\mathbb{1}$ is the singleton set.

One could directly define the limit $\lim_{n \to \infty} (-)(n)$ as a partial function

$\lim_{n \to \infty} (-)(n) \in (\mathbb{N} \to S) \to_{\mathcal{U}} S$

### In homotopy type theory

Let $S$ be a sequential convergence space. Then $S$ is a sequentially Hausdorff space if for all sequences $x:\mathbb{N} \to S$, the type of all limits of $x$ is a proposition

$isSequentiallyHausdorff(S) \coloneqq \prod_{x:\mathbb{N} \to S} isProp\left(\sum_{l:S} x \to l\right)$

One could directly define the limit $\lim_{n \to \infty} (-)(n)$ as a partial function

$\lim_{n \to \infty} (-)(n): (\mathbb{N} \to S) \to_{\mathcal{U}} S$

## Properties

Every Archimedean ordered field is a sequentially Hausdorff space.