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

Showing changes from revision #2 to #3: Added | Removed | Changed

# Contents

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

## Examples

• Everysequence

Every sequence $a: \mathbb{N} \to A$ is a net.

$a: \mathbb{N} \to A$ is a net.
• 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}_+$.