Homotopy Type Theory preconvergence space > history (Rev #1)

Idea
Definition
- In set theory
- In homotopy type theory
See also

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

Idea

The most general space where the notion of convergence and limit makes sense, but the term “convergence space” is already taken to mean a set with filters that are isotone, centered, and directed, and that definition is not the most general definition for which the notions of convergence and limit makes sense.

Definition

In set theory

A set $S$ is a preconvergence space if it comes with a binary relation $isLimit_S(-,-)$ between the (large) set of all nets in $S$

\bigcup_{I \in DirectedSet_\mathcal{U}} S^I

and $S$ itself.

In homotopy type theory

A type $S$ is a preconvergence space if it comes with a binary relation $isLimit_S(-,-)$ between the type of all nets in $S$

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