# Homotopy Type Theory net > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

# Contents

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

## Definition

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.

### In set theory

A sequence net is a net function whose index type is thenatural numbers$a \in A^I$ from a directed set \mathbb{N} I to a set $A$. $I$ is called the index set, the terms of $I$ are called indices (singular index), and $A$ is called the indexed set.

A sequence is a net whose index set is the natural numbers $\mathbb{N}$.

### In homotopy type theory

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.

A sequence is a net whose index type is the natural numbers $\mathbb{N}$.

## Examples

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