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.
See also constant morphism.
constant function / locally constant function