nLab dependent tuple

Redirected from "dependent tuple types".

Contents

Idea

In dependent type theory, given a natural number n:n:\mathbb{N}, an nn-tuple in a type AA is a family of elements i:Fin(n)x(i):Ai:\mathrm{Fin}(n) \vdash x(i):A, or equivalently, a function x:Fin(n)Ax:\mathrm{Fin}(n) \to A with domain of the finite set with nn elements. A dependent sequence is like a sequence but in which we allow AA to depend on the finite set.

Definition

Given a natural number n:n:\mathbb{N} and a family of types indexed by the finite set with nn elements i:Fin(n)A(i)i:\mathrm{Fin}(n) \vdash A(i), a dependent nn-tuple can be defined as

  • a family of elements i:Fin(n)x(i):A(i)i:\mathrm{Fin}(n) \vdash x(i):A(i)

  • an element of the dependent function type x:(i:Fin(n))A(i)x:(i:\mathrm{Fin}(n)) \to A(i)

Dependent n-tuple types

A dependent nn-tuple type is simply the dependent function type (i:Fin(n))A(i)(i:\mathrm{Fin}(n)) \to A(i), and thus comes with the following rules:

Formation rules for dependent tuple types:

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

Introduction rules for dependent tuple types:

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

Elimination rules for dependent tuple types:

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

Computation rules for dependent tuple types:

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

Uniqueness rules for dependent tuple types:

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

Properties

Dependent nn-tuple types also have their own extensionality principle, called dependent nn-tuple extensionality. This states that given two dependent nn-tuples a:(i:Fin(n))A(i)a:(i:\mathrm{Fin}(n)) \to A(i) and b:(i:Fin(n))A(i)b:(i:\mathrm{Fin}(n)) \to A(i) there is an equivalence of types between the identity type a= (i:Fin(n))A(i)ba =_{(i:\mathrm{Fin}(n)) \to A(i)} b and the dependent tuple type (i:Fin(n))(a(i)= A(i)b(i))(i:\mathrm{Fin}(n)) \to (a(i) =_{A(i)} b(i)):

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

Dependent nn-tuple extensionality is provable in any dependent type theory with dependent sum types and identity types; it follows from the same principles as product extensionality does.

Dependent tuple types are also used in defining finite choice in dependent type theory:

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

Similarly to dependent tuple extensionality, finite choice is provable in dependent type theory.

 See also

Created on January 9, 2023 at 23:16:51. See the history of this page for a list of all contributions to it.