Showing changes from revision #10 to #11:
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 type, letpreordered type . be Given a directed term type, and let , be the a positive net. cone Given of a term , the with positive respect cone to of with respect to is defined as the type
with monic function such that for all terms , .
Given a subtype net of and a net , with we monic say function that , is asubnet is ofeventually in if if comes with a function comes and with a term dependent function and such a that function for every dependent term , such there that is for a all dependent terms identification, .