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

In set theory

A sequence net is a net function whose index type is thenatural numbersaA Ia \in A^I from a directed set I \mathbb{N} I to a set AA. II is called the index set, the terms of II are called indices (singular index), and AA 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: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.

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

Examples

See also

Revision on April 14, 2022 at 01:36:56 by Anonymous?. See the history of this page for a list of all contributions to it.