Contents

# Contents

## Idea

The type-theoretic version of the fact that in set theory functions preserve equality between elements in sets.

## Definition

### Basic definition

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

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

defined by Id-induction from

$ap_f\big(refl_a\big) \,\equiv\, refl_{f(a)}$

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 : ### As the non-dependent version of the dependent function application to identifications

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)$.

### Inductive definition

If the function application to identifications is inductively defined, then it comes with rules saying that the following judgment can be formed

$a:A \vdash \mathrm{ap}_{f}(a, a)(\mathrm{refl}_{A}(a)) \equiv \mathrm{refl}_{B}(f(a)):\Omega(B, f(a))$

where $\Omega(A, a)$ is the loop space type $a =_A a$ of $A$ at $a:A$.

### Binary function applications to identifications

Given types $A$, $B$, and $C$ and a binary function $x:A, y:B \vdash f(x, y):C$, there is a dependent function

$a:A, a':A, b:B, b':B, p:a =_A a', q:b =_B b' \vdash \mathrm{apbinary}_f(a, a', b, b')(p, q):f(a, b) =_C f(a', b')$

called the binary function application to identifications or binary action on identifications (Rijke (2022), §19.5), inductively defined by

$a:A, b:B \vdash \mathrm{apbinary}_{f}(a, a, b, b)(\mathrm{refl}_{A}(a), \mathrm{refl}_{B}(b)) \equiv \mathrm{refl}_{C}(f(a, b)):\Omega(C, f(a, b))$

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})$.

### Finitary function application to identifications

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

$n:\mathbb{N}, x:\left(\prod_{i:\mathrm{Fin}(n)} A(i)\right) \vdash f(x):B$

there is a dependent function

$n:\mathbb{N}, a:\prod_{i:\mathrm{Fin}(n)} A(i), b:\prod_{i:\mathrm{Fin}(n)} A(i) \vdash \mathrm{ap}_f(n)(a, b):\left(\prod_{i:\mathrm{Fin}(n)} a(i) =_{A(i)} b(i)\right) \to f(a) =_{B} f(b)$