A net is a function from a directed type to a type . is called the index type, the terms of are called indices (singular index), and is called the indexed type.
Every sequence is a net.
The Cauchy approximations used to define the HoTT book real numbers are nets indexed by a dense subsemiring of the positive rational numbers .