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:IAa: I \to A from a directed type II to a type AA. II is called the index type, the terms of II are called indices (singular index), and AA is called the indexed type.

Examples

  • Everysequence

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

    a:Aa: \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 +R_{+} of the positive rational numbers +\mathbb{Q}_+.

See also

Revision on March 11, 2022 at 02:50:39 by Anonymous?. See the history of this page for a list of all contributions to it.