Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
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.
Subnets
Let be a preordered type. Given a term , the positive cone of with respect to is defined as the type
with monic function such that for all terms , .
Given a net and a net , we say that is a subnet of if comes with a function and a dependent function such that for every dependent term , there is a dependent identification .