conditionally constant functions

I'm proposing the name "conditionally constant" for a function that factors through the propositional truncation of its domain, to be distinguished from "weakly constant functions" which map all pairs of inputs to equal outputs and "constant functions" which factor through `Unit`.  This commit formalizes some basic facts about when weakly constant functions are conditionally constant, from the paper of Kraus, Escardo, Coquand, and Altenkirch.
We could.  I didn't have anything very interesting to say about them yet.  We do already have `const`.