nLab dependent sequence

Redirected from "dependent sequence types".

Contents

Idea

In dependent type theory, a sequence in a type AA is a family of elements n:x(n):An:\mathbb{N} \vdash x(n):A, or equivalently, a function x:Ax:\mathbb{N} \to A with domain of the natural numbers. A dependent sequence is like a sequence but in which we allow AA to depend on the natural numbers.

 Definition

Given a family of types indexed by the natural numbers n:A(n)n:\mathbb{N} \vdash A(n), a dependent sequence can be defined as

  • a family of elements n:x(n):A(n)n:\mathbb{N} \vdash x(n):A(n)

  • a dependent sequential net (x:P(x);x:,p:P(x)f(x,p):B(x),x:isInhab(x):[P(x)])(x:\mathbb{N} \vdash P(x); x:\mathbb{N}, p:P(x) \vdash f(x, p):B(x), x:\mathbb{N} \vdash \mathrm{isInhab}(x):\left[P(x)\right]) for which the dependent type P(x)P(x) is a contractible type for all natural numbers x:x:\mathbb{N}

  • a dependent correspondence x:,y:B(x)R(x,y)x:\mathbb{N}, y:B(x) \vdash R(x, y) for which the dependent type y:B(x)R(x,y)\sum_{y:B(x)} R(x, y) is a contractible type for all natural numbers x:x:\mathbb{N}.

  • an element of the dependent function type x:(n:)A(n)x:(n:\mathbb{N}) \to A(n)

Dependent sequence types

A dependent sequence type is simply the dependent function type (n:)A(n)(n:\mathbb{N}) \to A(n), and thus comes with the following rules:

Formation rules for dependent sequence types:

Γ,n:A(n)typeΓ(n:)A(n)type\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash (n:\mathbb{N}) \to A(n) \; \mathrm{type}}

Introduction rules for dependent sequence types:

Γ,n:A(n)typeΓ,n:a(n):A(n)Γλ(n:).a(n):(n:)A(n)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A(n)}{\Gamma \vdash \lambda(n:\mathbb{N}).a(n):(n:\mathbb{N}) \to A(n)}

Elimination rules for dependent sequence types:

Γ,n:A(n)typeΓ,a:(n:)A(n),n:ev(a,n):A(n)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma, a:(n:\mathbb{N}) \to A(n), n:\mathbb{N} \vdash \mathrm{ev}(a, n):A(n)}

Computation rules for dependent sequence types:

Γ,n:A(n)typeΓ,n:a(n):A(n)Γ,m:β Π(m):ev(λ(n:).a(n),m)= A(m)a(m)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type} \quad \Gamma, n:\mathbb{N} \vdash a(n):A(n)}{\Gamma, m:\mathbb{N} \vdash \beta_\Pi(m):\mathrm{ev}(\lambda(n:\mathbb{N}).a(n), m) =_{A(m)} a(m)}

Uniqueness rules for dependent sequence types:

Γ,n:A(n)typeΓ,a:(n:)A(n)η Π(a):a= (n:)A(n)λ(n:).a(n)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma, a:(n:\mathbb{N}) \to A(n) \vdash \eta_\Pi(a):a =_{(n:\mathbb{N}) \to A(n)} \lambda(n:\mathbb{N}).a(n)}

Dependent sequence types also have their own extensionality principle, called dependent sequence extensionality. This states that given two dependent sequences a:(n:)A(n)a:(n:\mathbb{N}) \to A(n) and b:(n:)A(n)b:(n:\mathbb{N}) \to A(n) there is an equivalence of types between the identity type a= (n:)A(n)ba =_{(n:\mathbb{N}) \to A(n)} b and the dependent sequence type (n:)(a(n)= A(n)b(n))(n:\mathbb{N}) \to (a(n) =_{A(n)} b(n)):

Γ,n:A(n)typeΓ,a:(n:)A(n),b:(n:)A(n)dseqext(a,b):(a= (n:)A(n)b)(n:)(a(n)= A(n)b(n))\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma,a:(n:\mathbb{N}) \to A(n), b:(n:\mathbb{N}) \to A(n) \vdash \mathrm{dseqext}(a, b):(a =_{(n:\mathbb{N}) \to A(n)} b) \simeq (n:\mathbb{N}) \to (a(n) =_{A(n)} b(n))}

Dependent sequence types are used in strongly predicative mathematics, where one does not have dependent function types, to construct the natural numbers type, as dependent sequence types are used in the elimination rules, computation rules, and uniqueness rules of the natural numbers type:

Elimination rules for the natural numbers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γind C(c 0,c s,n):C(n)\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(c_0, c_s, n):C(n)}

Computation rules for the natural numbers type:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γβ 0(c 0,c s):Id C(0)ind C(c 0,c s,0),c 0)\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \beta_\mathbb{N}^0(c_0, c_s):\mathrm{Id}_{C(0)}\mathrm{ind}_\mathbb{N}^C(c_0, c_s, 0), c_0)}
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γβ s(c 0,c s,n):Id C(s(n))(ind C(c 0,c s,s(n)),c s(n)(ind C(c 0,c s,n)))\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \beta_\mathbb{N}^s(c_0, c_s, n):\mathrm{Id}_{C(s(n))}(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, s(n)), c_s(n)(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, n)))}

Uniqueness rules for the natural numbers type:

Γ,x:C(x)typeΓc: x:C(x)Γn:Γη (c,n):Id C(n)(ind C(c(0),λx:.c(s(x)),n),c(n))\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{N}} C(x) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \eta_\mathbb{N}(c, n):\mathrm{Id}_{C(n)}(\mathrm{ind}_\mathbb{N}^C(c(0), \lambda x:\mathbb{N}.c(s(x)), n), c(n))}

It is also used in defining the axiom of countable choice in dependent type theory:

Γ,n:A(n)typeΓ,a:(n:)[A(n)]countablechoice(a):[(n:)A(n)]\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma, a:(n:\mathbb{N}) \to \left[A(n)\right] \vdash \mathrm{countablechoice}(a):\left[(n:\mathbb{N}) \to A(n)\right]}

 See also

Last revised on July 26, 2023 at 20:09:48. See the history of this page for a list of all contributions to it.