Given two sets and , there is a function such that for every element there is a function such that for every element , . For every element , the function is called the constant function from to with value .
Given two sets and and an element of , the constant function from to with value is the function defined by
for every element of .
More generally, any function is a constant function if
for every element and element of . Note that every constant function with particular value (as defined earlier) is constant (as defined here).
The converse is a little more complicated. If is inhabited, then every constant function from to is the constant function from to with some particular value, which is unique. If is empty but is inhabited, then the unique function from to is constant with any particular value in . If and are both empty, then the unique function from to is constant, but not constant at any particular value.
Using excluded middle, we can say that, if is inhabited, then any constant function from to is constant at some (possibly not unique) value, but this theorem fails in constructive mathematics.
See also constant morphism.
In dependent type theory, a propositionally constant function or typally constant function from type to at an element is a function such that for all . Equivalently, it is an element of the dependent sum type
For all , there is always a propositionally constant function given by with from the typal computation rules for function types, or
When function types have judgmental computation rules than one has .
Alternatively, a propositionally constant function is a function which factors through the base generator of the cone type of ; there exists a function such that for all , . Since the cone type of is always a contractible type, it is a terminal object in types.
Given a propositionally constant function with , by the recursion principle of the cone type, one has
such that
Last revised on December 27, 2023 at 16:04:42. See the history of this page for a list of all contributions to it.