**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 $A$ and $B$ and a family of elements $x:A \vdash f(x):B$, the function application to identifications for $f(x)$ is the family of elements

$a:A, b:A, p:a =_A b \vdash \mathrm{ap}_f(a, b, p):f(a) =_B f(b)$

A dependent function application to identifications is like an function application to identifications, but hwere we allow $B$ to depend on $x:A$ and similarly the identity type $f(a) =_B f(b)$ to be a heterogeneous identity type and depend on the identification $p:a =_A b$.

In dependent type theory, given a type $A$ and a type family $x:A \vdash B(x)$ and a family of elements $x:A \vdash f(x):B(x)$, the **dependent function application to identifications** or **dependent action on identifications** for $f(x)$ is the family of elements

$a:A, b:A, p:a =_A b \vdash \mathrm{apd}_f(a, b, p):\mathrm{hId}_{B}(a, b, p, f(a), f(b))$

inductively defined by

$a:A \vdash \mathrm{apd}_f(a, a, \mathrm{refl}_A(a)) \coloneqq \mathrm{hrefl}_A(a, f(a)):\mathrm{hId}_{B}(a, a, \mathrm{refl}_A(a), f(a), f(a))$

where $\mathrm{hId}_{B}(a, b, p, f(a), f(b))$ is a heterogeneous identity type.

If dependent identification types are defined in terms of function types from the interval type; i.e.

$p:\mathbb{I} \to A, x:B(p(0)), y:B(p(1)) \vdash \mathrm{apd}_f(p):\mathrm{hId}_{B}(p, x, y)$

then dependent function application is defined slightly differently.

By the recursion rule of the interval type, one could use a function $p:\mathbb{I} \to A$ instead of elements $a:A$, $b:A$, and identification $p:a =_A b$. Then given a type $A$ and a type family $x:A \vdash B(x)$ and a family of elements $x:A \vdash f(x):B(x)$, the **dependent function application to identifications** or **dependent action on identifications** for $f(x)$ is the family of elements

$p:\mathbb{I} \to A \vdash \mathrm{apd}_f(p):\mathrm{hId}_{B}(p, f(p(0)), f(p(1)))$

inductively defined using the induction principle of the path type $\mathbb{I} \to A$ by

$a:A \vdash \mathrm{apd}_f(\lambda i:\mathbb{I}.a) \coloneqq \mathrm{hrefl}_A(a, f(a)):\mathrm{hId}_{B}(\lambda i:\mathbb{I}.a, f(a), f(a))$

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 heterogeneous identity types:

$a:A, b:A, p:a =_A b \vdash \mathrm{apdl}_f(a, b, p):f(a) =_{B(a)} \mathrm{tr}_B(a, b, p)^{-1}(f(b))$

$a:A, b:A, p:a =_A b \vdash \mathrm{apdr}_f(a, b, p):\mathrm{tr}_B(a, b, p)(f(a)) =_{B(b)} f(b)$

Having one of the three notions of dependent function application to identifications means that one could define all three of them, because the types $f(a) =_B^p f(b)$, $f(a) =_{B(a)} \mathrm{tr}_B(a, b, p)^{-1}(f(b))$, and $\mathrm{tr}_B(a, b, p)(f(a)) =_{B(b)} f(b)$ are all equivalent to each other.

Last revised on December 26, 2023 at 20:19:33. See the history of this page for a list of all contributions to it.