## Not every weakly constant function is conditionally constant

Posted: June 16, 2015 in Uncategorized Homotopy Type Theory

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