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
The type-theoretic version of the fact that in set theory functions preserve equality between elements in sets.
In dependent type theory, given types $A$ and $B$ and a function $x \colon A \vdash f(x) \colon B$, there is induced a dependent function between the corresponding identity types
defined by Id-induction from
and called the application or action of $f$ to/on identities/identifications/equalities/paths [e.g. UFP (2013, p. 69), Rijke (2022, §5.3)].
By repeated Id-induction it readily follows, stagewise (e.g. UFP13, Lem 2.2.1), that $ap_f$ respects the concatenation, and the inversion of identifications, up to coherent higher-order identifications, hence that it acts as an $\infty$-functor on the $\infty$-groupoid-structure on homotopy types :
The function application to identifications is a special case of the dependent function application to identifications for which the type family $x:A \vdash B$ is a constant type family, and thus the dependent identity type $f(a) =_B^p f(b)$ doesn’t depend on the path $p:a =_A b$ and is thus a normal identity type $f(a) =_B f(b)$.
If the function application to identifications is inductively defined, then it comes with rules saying that the following judgment can be formed
where $\Omega(A, a)$ is the loop space type $a =_A a$ of $A$ at $a:A$.
Given types $A$, $B$, and $C$ and a binary function $x:A, y:B \vdash f(x, y):C$, there is a dependent function
called the binary function application to identifications or binary action on identifications (Rijke (2022), §19.5), inductively defined by
where $\Omega(A, a)$ is the loop space type $a =_A a$ of $A$ at $a:A$.
Binary function applications to identifications are used in proving product extensionality for product types, as well as defining multiplication on the integers $\mathrm{apbinary}_{\mu}:\mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$ from multiplication on the circle type $\mu:S^1 \times S^1 \to S^1$ when the integers are defined as the loop space type of the element $\mathrm{base}:S^1$, $\mathbb{Z} \coloneqq \Omega(S^1, \mathrm{base})$.
Let $n$ be a natural number, let $A$ be a family of types indexed by the finite type with $n$ elements $\mathrm{Fin}(n)$, and let $B$ be a type. Then given a function
there is a dependent function
Univalent Foundations Project, §2.2 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, §5.3 in: Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
Last revised on January 23, 2023 at 19:31:21. See the history of this page for a list of all contributions to it.