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

Showing changes from revision #9 to #10: Added | Removed | Changed

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

Eventuality

In homotopy type theory

Let AA be a type, let II be a directed type, and let a:IAa: I \to A be a net. Given a term i:Ii:I, the positive cone of II with respect to ii is defined as the type

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.

I i + j:IijI^+_i \coloneqq \sum_{j:I} i \leq j

with monic function f:I i +If:I^+_i \to I such that for all terms j:Ij:I, if(j)i \leq f(j).

Given a subtype BB of AA with monic function g:BAg:B \to A, aa is eventually in BB if II comes with a term i:Ii:I and a function b:I i +Bb:I^+_i \to B such that for all terms j:I i +j:I^+_i, a f(j)=g(b j)a_{f(j)} = g(b_j).

Examples

See also

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