nLab constant function

Redirected from "propositionally constant function".
Contents

Contents

Definition

Given two sets SS and TT, there is a function c:T(ST)c:T \to (S \to T) such that for every element x:Tx:T there is a function c(x):STc(x):S \to T such that for every element a:Sa:S, c(x)(a)=xc(x)(a) = x. For every element x:Tx:T, the function c(x)c(x) is called the constant function from SS to TT with value xx.

Given two sets SS and TT and an element xx of TT, the constant function from SS to TT with value xx is the function ff defined by

f(a)=x f(a) = x

for every element aa of SS.

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

f(a)=f(b) f(a) = f(b)

for every element aa and element bb of SS. Note that every constant function with particular value (as defined earlier) is constant (as defined here).

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

Using excluded middle, we can say that, if TT is inhabited, then any constant function from SS to TT 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 AA to BB at an element b:Bb:B is a function f:ABf:A \to B such that f(x)= Bbf(x) =_B b for all x:Ax:A. Equivalently, it is an element of the dependent sum type

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

For all b:Bb:B, there is always a propositionally constant function given by λx:A.b:AB\lambda x:A.b:A \to B with β A,B x:A.b: x:A(λx:A.b)(x)= Bb\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,λx:A.b,β A,B x:A.b): b:B f:AB x:Af(x)= Bb(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 β A,B x:A.bλx:A.refl B(b)\beta_{A, B}^{x:A.b} \equiv \lambda x:A.\mathrm{refl}_B(b).

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

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

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

such that

rec Cone(A) B(b,f,p)(vertex)b:B\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p)(\mathrm{vertex}) \equiv b:B
rec Cone(A) B(b,f,p)(base(x))f(x):B\mathrm{rec}_{\mathrm{Cone}(A)}^B(b, f, p)(\mathrm{base}(x)) \equiv f(x):B
ap rec Cone(A) B(b,f,p)(edge(x))p:f(x)= Bb\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.