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

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

Eventuality Subnets

Let A I A I be a type, letIIpreordered type . be Given a directed term type, and let a i:IA a: i:I I \to A , be the a positive net. cone Given of a termi:I i:I I , the with positive respect cone to of I i I i 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 net B a:IA B a: I \to A of and a netb:JA b:J \to A , with we monic say function that g b:BA g:B b \to A , is aaasubnet is ofeventuallyaa in if B b B b if comes with a functionf:IJ I f:I \to J comes and with a term dependent function i g: i:IJ f(i) +I i:I g:\prod_{i:I} J^+_{f(i)} \to I and such a that function for every dependent term b j(i): I J if(i) +B b:I^+_i j(i):J^+_{f(i)} \to B , such there that is for a all dependent terms identificationp(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)a_{f(j)} = g(b_j).

ba i:I k:J(f(i)k)×[ l:I(il)×(a k=b l)]b \subseteq a \coloneqq \prod_{i:I} \prod_{k:J} (f(i) \leq k) \times \left[\sum_{l:I} (i \leq l) \times (a_k = b_l)\right]

Examples

See also

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