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
In dependent type theory, given types and and a family of elements , the function application to identifications for is the family of elements
A dependent function application to identifications is like an function application to identifications, but hwere we allow to depend on and similarly the identity type to be a indexed heterogeneous identity type and depend on the identification .
In dependent type theory, given a type and a type family and a family of elements , the dependent function application to identifications or dependent action on identifications for is the family of elements
inductively defined by
where is a indexed heterogeneous identity type.
If dependent identification types are defined in terms of function types from the interval type; i.e.
then dependent function application is defined slightly differently.
By the recursion rule of the interval type, one could use a function instead of elements , , and identification . Then given a type and a type family and a family of elements , the dependent function application to identifications or dependent action on identifications for is the family of elements
inductively defined using the induction principle of the path type by
In addition, there are two other families of elements which could be considered dependent function applications to identifications, which use transport and the inverse of transport rather than indexed heterogeneous identity types:
Having one of the three notions of dependent function application to identifications means that one could define all three of them, because the types , , and are all equivalent to each other.
One can also consider dependent function application to identifications of arity , , given a family of elements indexed by type . We have, for a dependent function , a reflexive family
and thus by identification induction of the indexed heterogeneous identity type of arity , we have a function
called the application of the dependent function to identifications of arity or the action of dependent function on identifications of arity , such that for all ,
Univalent Foundations Project, §2.3 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, §5.4 in: Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
Last revised on July 3, 2025 at 21:24:43. See the history of this page for a list of all contributions to it.