Homotopy Type Theory Hausdorff space > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In premetric spaces
- Most general definition
See also

Definition

In premetric spaces

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and $R_{+}$ be the positive terms of $R$ .

Let $S$ be an $R_{+}$ -premetric space. Then $S$ is a Hausdorff space if for all directed types $I:\mathcal{U}$ and nets $x:I \to S$ , the type of all limits of $x$ is a proposition

p isHausdorff : (S) ≔ \prod_{I : 𝒰} isDirected (I) \times \prod_{x : I \to S} isProp (\lim x)

~~p:\prod_{I:\mathcal{U}}~~ isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isProp(\lim x)

Most general definition

Let $S$ be a type with a predicate $\to$ between the type of all nets in $S$

\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and $S$ itself. Then $S$ is a Hausdorff space if for all directed types $I:\mathcal{U}$ and nets $x:I \to S$ , the type of all limits of $x$ is a proposition

p isHausdorff : (S) ≔ \prod_{I : 𝒰} isDirected (I) \times \prod_{x : I \to S} isProp ((\sum_{l : S} x \to l) \lim x)

~~p:\prod_{I:\mathcal{U}}~~ isHausdorff(S) \coloneqq \prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} ~~isProp(\lim~~ isProp\left(\sum_{l:S} x) x \to l\right)

One could directly define the limit $\lim$ as a partial function

\lim: \left(\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)\right) \to_{\mathcal{U}^+} S

Homotopy Type Theory Hausdorff space > history (Rev #4, changes)

Contents

Definition

In premetric spaces

Most general definition

See also