Showing changes from revision #11 to #12:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
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.
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 .
Last revised on June 10, 2022 at 01:47:49. See the history of this page for a list of all contributions to it.