Homotopy Type Theory net > history (Rev #10)


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


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.


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

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


See also

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