Showing changes from revision #10 to #11:
Added | ~~Removed~~ | ~~Chan~~ged

Whenever editing is allowed on the nLab again, this article should be ported over there.

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

Let $\mathrm{AI}$~~ A~~ I be a~~ type,~~~~ let~~~~$I$~~preordered type~~ ~~ .~~ be~~ Given a~~ directed~~ term~~ type,~~~~ and~~~~ let~~$\mathrm{ai}:I\to A$~~ a:~~ i:I~~ I~~~~ \to~~~~ A~~~~ ~~ ,~~ be~~ the~~ a~~ positive~~ net.~~ cone~~ Given~~ of~~ a~~~~ term~~$i:I$~~ i:I~~ I~~ ,~~ ~~ the~~ with~~ positive~~ respect~~ cone~~ to~~ of~~$\mathrm{Ii}$~~ I~~ i~~ with respect to ~~~~$i$~~ is defined as the type

$I^+_i \coloneqq \sum_{j:I} i \leq j$

with monic function $f:I^+_i \to I$ such that for all terms $j:I$, $i \leq f(j)$.

Given a~~ subtype~~ net$\mathrm{Ba}:I\to A$~~ B~~ a: I \to A ~~ of~~ and a net$b:J\to A$ b:J \to A~~ ~~ ,~~ with~~ we~~ monic~~ say~~ function~~ that$\mathrm{gb}:B\to A$~~ g:B~~ b~~ \to~~~~ A~~~~ ,~~ is a~~$a$~~**subnet** ~~ is~~ of$a$ **eventually**~~ in~~ if$\mathrm{Bb}$~~ B~~ b ~~ if~~ comes with a function$f:I\to J$~~ I~~ f:I \to J ~~ comes~~ and~~ with~~ a~~ term~~ dependent function$\mathrm{ig}:{\prod}_{i:I}{J}_{f(i)}^{+}\to I$~~ i:I~~ g:\prod_{i:I} J^+_{f(i)} \to I ~~ and~~ such~~ a~~ that~~ function~~ for every dependent term$\mathrm{bj}(i):{\mathrm{IJ}}_{i}^{f(i)}\to B$~~ b:I^+_i~~ j(i):J^+_{f(i)}~~ \to~~~~ B~~~~ ~~ ,~~ such~~ there~~ that~~ is~~ for~~ a~~ all~~ dependent~~ terms~~ identification$p(i,j(i)):{I}_{i}^{+}{a}_{j(i)}={b}_{g(i)(j(i))}$~~ j:I^+_i~~ p(i, j(i)): a_{j(i)} = b_{g(i)(j(i))}~~, ~~~~$a_{f(j)} = g(b_j)$~~.

$b \subseteq a \coloneqq \prod_{i:I} \prod_{k:J} (f(i) \leq k) \times \left[\sum_{l:I} (i \leq l) \times (a_k = b_l)\right]$

- 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}_+$.