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

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**.

~~Every~~~~sequence~~Every sequence $a: \mathbb{N} \to A$ is a net.

~~$a: \mathbb{N} \to A$~~~~is a net.~~-
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}_+$.