Showing changes from revision #10 to #11: 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: I \to A$ from a directed type $I$ to a type $A$. $I$ is called the index type, the terms of $I$ are called indices (singular index), and $A$ is called the indexed type.

Eventuality Subnets

Let $\mathrm{<span><del\; class="diffmod">\; A</del><ins\; class="diffmod">\; I</ins></span>}$ A I be a type, let$I$preordered type . be Given a directed term type, and let$\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; i</ins></span>}:I\to A$ a: i:I I \to A , be the a positive net. cone Given of a term$i:I$ i:I I , the with positive respect cone to of$\mathrm{<span><del\; class="diffmod">\; I</del><ins\; class="diffmod">\; i</ins></span>}$ I i with respect to $i$ is defined as the type

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

Given a subtype net$\mathrm{<span><del\; class="diffmod">\; B</del><ins\; class="diffmod">\; a</ins></span>}:I\to A$ B a: I \to A of and a net$b:J\to A$ b:J \to A , with we monic say function that$\mathrm{<span><del\; class="diffmod">\; g</del><ins\; class="diffmod">\; b</ins></span>}:B\to A$ g:B b \to A , is a$a$subnet is ofeventually$a$ in if$\mathrm{<span><del\; class="diffmod">\; B</del><ins\; class="diffmod">\; b</ins></span>}$ B b if comes with a function$f:I\to J$ I f:I \to J comes and with a term dependent function$\mathrm{<span><del\; class="diffmod">\; i</del><ins\; class="diffmod">\; g</ins></span>}:{\prod }_{i:I}{J}_{f(i)}^{+}\to I$ i:I g:\prod_{i:I} J^+_{f(i)} \to I and such a that function for every dependent term$\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; j</ins></span>}(i):{\mathrm{<span><del\; class="diffmod">\; I</del><ins\; class="diffmod">\; J</ins></span>}}_i^{f(i)}\to B$ b:I^+_i j(i):J^+_{f(i)} \to B , such there that is for a all dependent terms identification$p(i,j(i)):I_i^{+}{a}_{j(i)}=b_{g(i)(j(i))}$ j:I^+_i p(i, j(i)): a_{j(i)} = b_{g(i)(j(i))}, $a_{f(j)} = g(b_j)$.