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

Showing changes from revision #5 to #6: 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.

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

Examples

See also

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