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.
Hmm, that didn't occur to me.  We could use `Fixpoints`.  Another option would be something like `split_wconst`, since a weakly constant endofunction is in fact idempotent and this is its splitting.  (In fact, an endofunction is weakly constant iff it is idempotent and its splitting is an hprop.)