As discussed at length on the mailing list some time ago, there are several different things that one might mean by saying that a function $latex f:Ato B$ is “constant”. Here is my preferred terminology:

- $latex f$ is
**constant**if we have $latex b:B$ such that $latex f(a)=b$ for all $latex a:A$.

This is equivalent to saying that $latex f$ factors through $latex mathbf{1}$. - $latex f$ is
**conditionally constant**if it factors through $latex Vert A Vert$. - $latex f$ is
**weakly constant**if for all $latex a_1,a_2:A$ we have $latex f(a_1)=f(a_2)$.

In particular, the identity function of $latex emptyset$ is conditionally constant, but not constant. I don’t have a problem with that; getting definitions right often means that they behave slightly oddly on the empty set (until we get used to it). The term “weakly constant” was introduced by Kraus, Escardo, Coquand, and Altenkirch, although they immediately dropped the…

View original post 1,189 more words

Advertisements