[[!redirects nets]] #Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|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 $$I^+_i \coloneqq \sum_{j:I} i \leq j$$ 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]]