nLab constant function

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.

See also constant morphism.

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

Related concepts

• constant of a theory

• constant function / locally constant function

• constant sheaf / locally constant sheaf

• constant stack / locally constant stack

• constant ∞-stack / locally constant ∞-stack

• local system

• weakly constant function

• deterministic random variable, almost surely

• cone type