dependent tuple (changes) in nLab

Showing changes from revision #0 to #1: Added | Removed | Changed

\tableofcontents

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

• tuple, sequence, function

• dependent tuple, dependent sequence, dependent function

• finite choice