Showing changes from revision #11 to #12:
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 $I$ be a preordered type. Given a term $i:I$, the positive cone of $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 net $a: I \to A$ and a net $b:J \to A$, we say that $b$ is a **subnet** of $a$ if $b$ comes with a function $f:I \to J$ and a dependent function $g:\prod_{i:I} J^+_{f(i)} \to I$ such that for every dependent term $j(i):J^+_{f(i)}$, there is a dependent identification $p(i, j(i)): a_{j(i)} = b_{g(i)(j(i))}$.

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

Last revised on June 10, 2022 at 01:47:49. See the history of this page for a list of all contributions to it.