Homotopy Type Theory net > history (Rev #9)

Contents

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

Definition

In set theory

A net is a function aA Ia \in A^I from a directed set II 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.

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.

Examples

See also

Revision on May 3, 2022 at 12:48:20 by Anonymous?. See the history of this page for a list of all contributions to it.