nLab sequential net

Redirected from "dependent sequential net".

Contents

Definition

In set theory

A sequential net is a multi-valued function from \mathbb{N} (or a decidable subset thereof) to XX, that is a span AX\mathbb{N} \leftarrow A \rightarrow X where the map AA \to \mathbb{N} is a surjection (or has a decidable range).

In type theory

A sequential net in a type BB can be defined as

  • a span with domain of the natural numbers, whose function into the natural numbers is a surjection, which consists of
    • a type CC
    • a family of elements z:Cg(z):z:C \vdash g(z):\mathbb{N}
    • a family of elements z:Ch(z):Bz:C \vdash h(z):B
    • a family of witnesses x:isInhab(x):[ z:Bg(z)= x]x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[\sum_{z:B} g(z) =_\mathbb{N} x\right] that each dependent type z:Bg(z)= x\sum_{z:B} g(z) =_\mathbb{N} x is inhabited for all natural numbers x:x:\mathbb{N}
  • a multivalued function with domain of the natural numbers, which consists of
    • a type family x:P(x)x:\mathbb{N} \vdash P(x)
    • a family of elements x:,p:P(x)f(x,p):Bx:\mathbb{N}, p:P(x) \vdash f(x, p):B
    • a family of witnesses x:isInhab(x):[P(x)]x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[P(x)\right] that each dependent type P(x)P(x) is inhabited for all natural numbers x:x:\mathbb{N}
  • a total correspondence with domain of the natural numbers, consisting of
    • a type family x:,y:BR(x,y)x:\mathbb{N}, y:B \vdash R(x, y)
    • a family of witnesses x:isInhab(x):[ y:BR(x,y)]x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[\sum_{y:B} R(x, y)\right] that each dependent type y:BR(x,y)\sum_{y:B} R(x, y) is inhabited for all natural numbers x:x:\mathbb{N}

Properties

Given a sequential net AA, AA inherits the structure of a directed set via AA \to \mathbb{N}, so that AXA \to X is a net. In the context of weak countable choice, as a net, every sequential net is equivalent (in the sense of corresponding to the same filter) to some sequence.

Without weak countable choice, many of the usual properties of metric spaces and other sequential spaces fail, but they continue to hold using sequential nets in the place of sequences. For example, every (located Dedekind) real number may be represented as a sequential Cauchy net, even when they might not all be represented as Cauchy sequences; see Cauchy real number.

Dependent sequential nets

A dependent sequential net is like a sequential net, but where we generalize from a single type BB to a family of types x:B(x)x:\mathbb{N} \vdash B(x) indexed by the natural numbers.

A dependent sequential net in a type family x:B(x)x:\mathbb{N} \vdash B(x) can be defined as

  • a dependent multivalued function with domain of the natural numbers, which consists of
    • a type family x:P(x)x:\mathbb{N} \vdash P(x)
    • a family of elements x:,p:P(x)f(x,p):B(x)x:\mathbb{N}, p:P(x) \vdash f(x, p):B(x)
    • a family of witnesses x:isInhab(x):[P(x)]x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[P(x)\right] that each dependent type P(x)P(x) is inhabited for all natural numbers x:x:\mathbb{N}
  • a total dependent correspondence with domain of the natural numbers, consisting of
    • a type family x:,y:B(x)R(x,y)x:\mathbb{N}, y:B(x) \vdash R(x, y)
    • a family of witnesses x:isInhab(x):[ y:B(x)R(x,y)]x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[\sum_{y:B(x)} R(x, y)\right] that each dependent type y:B(x)R(x,y)\sum_{y:B(x)} R(x, y) is inhabited for all natural numbers x:x:\mathbb{N}

See also

Last revised on January 10, 2023 at 07:10:11. See the history of this page for a list of all contributions to it.