[[!redirects sequence]] #Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### A __net__ is a function $a \in A^I$ from a directed set $I$ to a set $A$. $I$ is called the __index set__, the terms of $I$ are called __indices__ (singular __index__), and $A$ is called the __indexed set__. A __sequence__ is a net whose index set is the [[natural numbers]] $\mathbb{N}$. ### In homotopy type theory ### 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__. A __sequence__ is a net whose index type is the [[natural numbers]] $\mathbb{N}$. ## 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]] * [[Cauchy structure]] * [[Cauchy net]] * [[limit of a net]]