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.
In the proof that `X -> Contr P` implies `merely X -> IsHProp P`; applying truncation-recursion requires knowing that `IsHProp P` is itself an hprop, which requires funext.