Contents

# Contents

## Definition

Given two sets $S$ and $T$, there is a function $c:T \to (S \to T)$ such that for every element $x:T$ there is a function $c(x):S \to T$ such that for every element $a:S$, $c(x)(a) = x$. For every element $x:T$, the function $c(x)$ is called the constant function from $S$ to $T$ with value $x$.

Given two sets $S$ and $T$ and an element $x$ of $T$, the constant function from $S$ to $T$ with value $x$ is the function $f$ defined by

$f(a) = x$

for every element $a$ of $S$.

More generally, any function $f: S \to T$ is a constant function if

$f(a) = f(b)$

for every element $a$ and element $b$ of $S$. Note that every constant function with particular value (as defined earlier) is constant (as defined here).

The converse is a little more complicated. If $S$ is inhabited, then every constant function from $S$ to $T$ is the constant function from $S$ to $T$ with some particular value, which is unique. If $S$ is empty but $T$ is inhabited, then the unique function from $S$ to $T$ is constant with any particular value in $T$. If $S$ and $T$ are both empty, then the unique function from $S$ to $T$ is constant, but not constant at any particular value.

Using excluded middle, we can say that, if $T$ is inhabited, then any constant function from $S$ to $T$ is constant at some (possibly not unique) value, but this theorem fails in constructive mathematics.

### In dependent type theory

In dependent type theory, a propositionally constant function or typally constant function from type $A$ to $B$ at an element $b:B$ is a function $f:A \to B$ such that $f(x) =_B b$ for all $x:A$. Equivalently, it is an element of the dependent sum type

$\sum_{b:B} \sum_{f:A \to B} \prod_{x:A} f(x) =_B b$

For all $b:B$, there is always a propositionally constant function given by $\lambda x:A.b:A \to B$ with $\beta_{A, B}^{x:A.b}:\prod_{x:A} (\lambda x:A.b)(x) =_B b$ from the typal computation rules for function types, or

$(b, \lambda x:A.b, \beta_{A, B}^{x:A.b}):\sum_{b:B} \sum_{f:A \to B} \prod_{x:A} f(x) =_B b$

When function types have judgmental computation rules than one has $\beta_{A, B}^{x:A.b} \equiv \lambda x:A.\mathrm{refl}_B(b)$.

Alternatively, a propositionally constant function $f:A \to B$ is a function which factors through the base generator $\mathrm{base}:A \to \mathrm{Cone}(A)$ of the cone type of $A$; there exists a function $b:\mathrm{Cone}(A) \to B$ such that for all $x:A$, $b(\mathrm{base}(x)) \equiv f(x)$. Since the cone type of $A$ is always a contractible type, it is a terminal object in types.

Given a propositionally constant function $f:A \to B$ with $p:\prod_{x:A} f(x) =_B b$, by the recursion principle of the cone type, one has

$\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p):\mathrm{Cone}(A) \to B$

such that

$\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p)(\mathrm{vertex}) \equiv b:B$
$\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p)(\mathrm{base}(x)) \equiv f(x):B$
$\mathrm{ap}_{\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p)}(\mathrm{edge}(x)) \equiv p:f(x) =_B b$

Last revised on December 27, 2023 at 16:04:42. See the history of this page for a list of all contributions to it.