Contents

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

Definition

A net is a function $a: I \to A$ from a directed type $I$ to a type $A$. $I$ is called the index type, the terms of $I$ are called indices (singular index), and $A$ is called the indexed type.

Eventuality

Let $A$ be a type, let $I$ be a directed type, and let $a: I \to A$ be a net. Given a term $i:I$, the positive cone of $I$ with respect to $i$ is defined as the type

with monic function $f:I^+_i \to I$ such that for all terms $j:I$, $i \leq f(j)$.

Given a subtype $B$ of $A$ with monic function $g:B \to A$, $a$ is eventually in $B$ if $I$ comes with a term $i:I$ and a function $b:I^+_i \to B$ such that for all terms $j:I^+_i$, $a_{f(j)} = g(b_j)$.

Examples

• The Cauchy approximations used to define the HoTT book real numbers are nets indexed by a dense subsemiring $R_{+}$ of the positive rational numbers $\mathbb{Q}_+$.

See also

• directed type

• sequence

• Cauchy structure

• Cauchy net

• limit of a net