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

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s