nLab
dependent tuple
Redirected from "dependent tuple types".
Contents
Idea
In dependent type theory , given a natural number n : ℕ n:\mathbb{N} , an n n -tuple in a type A A is a family of elements i : Fin ( n ) ⊢ x ( i ) : A i:\mathrm{Fin}(n) \vdash x(i):A , or equivalently, a function x : Fin ( n ) → A x:\mathrm{Fin}(n) \to A with domain of the finite set with n n elements. A dependent sequence is like a sequence but in which we allow A A 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 n n elements i : Fin ( n ) ⊢ A ( i ) i:\mathrm{Fin}(n) \vdash A(i) , a dependent n n -tuple can be defined as
Dependent n-tuple types
A dependent n n -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 n n -tuple types also have their own extensionality principle, called dependent n n -tuple extensionality . This states that given two dependent n n -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 ) b a =_{(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 n n -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.