natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Let $\mathbb{N}$ be the set of natural numbers, let $n:\mathbb{N}$ be an arbitrary natural number, let $\mathrm{Fin}(n)$ be the finite set with $n$ elements, and let $A$ be an arbitrary set. Then $n$-tuple extensionality states that for every tuple $a:\mathrm{Fin}(n) \to A$ and $b:\mathrm{Fin}(n) \to A$, $a =_{\mathrm{Fin}(n) \to A} b$ if and only if $a(i) =_A b(i)$ for all elements $i \in \mathrm{Fin}(n)$.
In dependent type theory, $n$-tuple extensionality states that given two $n$-tuples $a:\mathrm{Fin}(n) \to A$ and $b:\mathrm{Fin}(n) \to A$ there is an equivalence of types between the identity type $a =_{\mathrm{Fin}(n) \to A} b$ and the dependent tuple type $(i:\mathrm{Fin}(n)) \to (a(i) =_{A} b(i))$:
There is also a version of $n$-tuple extensionality for dependent tuple types called dependent $n$-tuple extensionality, which states that given two dependent $n$-tuples $a:(i:\mathrm{Fin}(n)) \to A(i)$ and $b:(i:\mathrm{Fin}(n)) \to A(i)$ there is an equivalence of types between the identity type $a =_{(i:\mathrm{Fin}(n)) \to A(i)} b$ and the dependent tuple type $(i:\mathrm{Fin}(n)) \to (a(i) =_{A(i)} b(i))$:
Tuple extensionality is always true in set theory and dependent type theory, for the same reason that product extensionality is true.
Indeed, one could express tuple extensionality as two separate cases representing nullary tuples and binary tuples:
Every two elements in a singleton are equal to each other
product extensionality: Given two ordered pairs in a product set, they are equal if and only if the left product projections are equal to each other and the right product projections are equal to each other.
In dependent type theory, this becomes:
Every identity type of two elements in a contractible type is a contractible type.
product extensionality: Given two ordered pairs in a product set, the identity type between the two ordered pairs is equivalent to the product type of the identity type of the left product projections and the identity type of the right product projections.
Created on January 10, 2023 at 00:54:54. See the history of this page for a list of all contributions to it.